Module imports

Stream: general

[Washington Irving]

I am new to lean. I am attempting to prove the following:

theorem prob_union_le_sum_probs (A B : Set Ω) (prob : ProbabilityMeasure Ω) :
  prob (A ∪ B) ≤ prob A + prob B :=
begin
  -- Your proof goes here
end

How can I import ProbabilityMeasure? I tried

import Mathlib.MeasureTheory

but it does not resolve the entire module, it searches (and fails to find) Mathlib/MeasureTheory.lean.

Any idea how I can get this import, besides searching for and importing the exact file that contains ProbabilityMeasure?

[Ruben Van de Velde]

By importing the exact file that contains ProbabilityMeasure

[Ruben Van de Velde]

Or import Mathlib for the entire library

[Daniel Weber]

You can use import Mathlib to import everything. I recall some talk about files you can import for specific subjects, but I don't think that's implemented yet, so if you want something finer than import Mathlib you'll have to figure out the exact files to import.
Note that after using import Mathlib you can use #min_imports to find the relevant files

[Daniel Weber]

(By the way, ProbabilityMeasure is actually docs#MeasureTheory.ProbabilityMeasure, so you need to either open MeasureTheory/namespace MeasureTheory or use the full name. Additionally begin and end are Lean 3 syntax, you should do

theorem prob_union_le_sum_probs (A B : Set Ω) (prob : ProbabilityMeasure Ω) :
    prob (A ∪ B) ≤ prob A + prob B := by
  sorry

)

[Rémy Degenne]

Also you should probably not use ProbabilityMeasure, but instead a Measurewith property IsProbabilityMeasure. See https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ for an explanation (and more remarks about how to do probability in Mathlib).

[Washington Irving]

Thanks all for the suggestions. I was able to resolve my issue simply with:

import Mathlib