English
Let Ixx be a two-argument family of subsets of α and p a predicate. If the endpoints Ixx(a,b) satisfy certain nonemptiness and intersection properties, then for any s,t ⊆ α the collection { S | ∃ l ∈ s, ∃ u ∈ t, p(l,u) ∧ Ixx(l,u) = S } is a π-system.
Русский
Пусть Ixx — семейство подмножеств α двумя аргументами, и p — предикат. При условии, что Ixx(a,b) непусто и пересечения удовлетворяют заданному правилу, множество { S | ∃ l ∈ s, ∃ u ∈ t, p(l,u) ∧ Ixx(l,u) = S } образует π-систему.
LaTeX
$$$$ \mathrm{IsPiSystem}\left\{ S : \exists l \in s, \exists u \in t, p(l,u) \land Ixx(l,u) = S \right\} $$$$
Lean4
theorem isPiSystem_Ixx_mem {Ixx : α → α → Set α} {p : α → α → Prop} (Hne : ∀ {a b}, (Ixx a b).Nonempty → p a b)
(Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (s t : Set α) :
IsPiSystem {S | ∃ᵉ (l ∈ s) (u ∈ t), p l u ∧ Ixx l u = S} :=
by
rintro _ ⟨l₁, hls₁, u₁, hut₁, _, rfl⟩ _ ⟨l₂, hls₂, u₂, hut₂, _, rfl⟩
simp only [Hi]
exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩
