isPiSystem_Icc_mem — Mathlib

English

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

Русский

Пусть s ⊆ α, t ⊆ α. Набор Icc(l,u) с l ∈ s, u ∈ t, удовлетворяющий l ≤ u, образует π-систему.

LaTeX

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

Lean4

theorem isPiSystem_Icc_mem (s t : Set α) : IsPiSystem {S | ∃ᵉ (l ∈ s) (u ∈ t), l ≤ u ∧ Icc l u = S} :=
  isPiSystem_Ixx_mem (Ixx := Icc) nonempty_Icc.1 (by exact Icc_inter_Icc) s t

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