isPiSystem_Ioo_mem — Mathlib

English

Let s,t ⊆ α. Then the set of all Ioo-intervals between elements of s and t forms a π-system: { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ioo(l,u) = S }.

Русский

Пусть s,t ⊆ α. Тогда множество интервалов Ioo между элементами s и t образует π-систему: { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ioo(l,u) = S }.

LaTeX

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

Lean4

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

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