biInter_mem — Mathlib

English

An algebra is closed under finite intersections.

Русский

Алгебра замкнута относительно конечных пересечений.

LaTeX

$$$\\forall S : Finset, (\\forall i \\in S, s_i \\in 𝒜) \\Rightarrow \\bigcap_{i \\in S} s_i \\in 𝒜$$$

Lean4

/-- An algebra of sets is closed by finite intersections. -/
theorem biInter_mem {ι : Type*} (h𝒜 : IsSetAlgebra 𝒜) {s : ι → Set α} (S : Finset ι) (hs : ∀ i ∈ S, s i ∈ 𝒜) :
    ⋂ i ∈ S, s i ∈ 𝒜 := by
  by_cases h : S = ∅
  · rw [h, ← Finset.set_biInter_coe, Finset.coe_empty, biInter_empty]
    exact h𝒜.univ_mem
  · rw [← ne_eq, ← Finset.nonempty_iff_ne_empty] at h
    exact h𝒜.isSetRing.biInter_mem S h hs

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