Theorems · Theorem · measure theory

isPiSystem_Ixx

∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop},
  (∀ {a b : α}, (Ixx a b).Nonempty → p a b) →
    (∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) →
      ∀ (f : ι → α) (g : ι' → α), IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}

Defined in

Mathlib.MeasureTheory.PiSystem

Cited by

4 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

LinearOrder