isPiSystem_Ico_mem — Mathlib

English

Let s,t ⊆ α. The sets Ico(l,u) with l ∈ s and u ∈ t form a π-system: { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico(l,u) = S }.

Русский

Пусть s ⊆ α, t ⊆ α. Набор Ico(l,u) с l ∈ s, u ∈ t образует π-систему: { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico(l,u) = S }.

LaTeX

$$$$ \mathrm{IsPiSystem}\left(\{ S : \exists l \in s, \exists u \in t, l < u \land Ico(l,u) = S \}\right) $$$$

Lean4

theorem isPiSystem_Ico_mem (s t : Set α) : IsPiSystem {S | ∃ᵉ (l ∈ s) (u ∈ t), l < u ∧ Ico l u = S} :=
  isPiSystem_Ixx_mem (Ixx := Ico) (fun ⟨_, hax, hxb⟩ => hax.trans_lt hxb) Ico_inter_Ico s t

Похожие утверждения