Loogle!
Result
Found 7 definitions mentioning MeasurableSet.iUnion.
- MeasurableSet.iUnion Mathlib.MeasureTheory.MeasurableSpace.Defs
∀ {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [inst : Countable ι] ⦃f : ι → Set α⦄, (∀ (b : ι), MeasurableSet (f b)) → MeasurableSet (⋃ b, f b) - MeasureTheory.inducedOuterMeasure_eq Mathlib.MeasureTheory.OuterMeasure.Induced
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0), (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) → ∀ {s : Set α} (hs : MeasurableSet s), (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs - MeasureTheory.inducedOuterMeasure_eq_extend Mathlib.MeasureTheory.OuterMeasure.Induced
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0), (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) → ∀ {s : Set α}, MeasurableSet s → (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s - MeasureTheory.extend_mono Mathlib.MeasureTheory.OuterMeasure.Induced
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal}, m ∅ ⋯ = 0 → (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) → ∀ {s₁ s₂ : Set α}, MeasurableSet s₁ → s₁ ⊆ s₂ → MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂ - MeasureTheory.extend_iUnion_le_tsum_nat Mathlib.MeasureTheory.OuterMeasure.Induced
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal}, m ∅ ⋯ = 0 → (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) → ∀ (s : ℕ → Set α), MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i) - MeasureTheory.Measure.ofMeasurable Mathlib.MeasureTheory.Measure.MeasureSpaceDef
{α : Type u_1} → [inst : MeasurableSpace α] → (m : (s : Set α) → MeasurableSet s → ENNReal) → m ∅ ⋯ = 0 → (∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) → MeasureTheory.Measure α - MeasureTheory.Measure.ofMeasurable_apply Mathlib.MeasureTheory.Measure.MeasureSpaceDef
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} {m0 : m ∅ ⋯ = 0} {mU : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯} (s : Set α) (hs : MeasurableSet s), (MeasureTheory.Measure.ofMeasurable m m0 mU) s = m s hs
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→
and∀
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 7eaed1d
serving mathlib revision 2a811d0