inter_eq_iInter — Mathlib

English

For sets s1 and s2, their intersection equals the iInter over booleans of conditional selections: s1 ∩ s2 = ⋂ b : Bool, cond b s1 s2.

Русский

Для множеств s1 и s2 их пересечение равно iInter по булеву индексу: s1 ∩ s2 = ⋂ b : Bool, cond b s1 s2.

LaTeX

$$$$ \\bigcap_{i} s_{1} \\cap s_{2} = \\bigcap_{b : \\text{Bool}} \\operatorname{cond} (b)\\, s_{1}\\, s_{2}. $$$$

Lean4

theorem inter_eq_iInter {s₁ s₂ : Set α} : s₁ ∩ s₂ = ⋂ b : Bool, cond b s₁ s₂ :=
  inf_eq_iInf s₁ s₂

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