isPiSystem_Ioc_mem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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