isOpen_sInter — Mathlib

English

If s is finite and each t ∈ s is open, then the intersection ⋂₀ s is open.

Русский

Если s конечно, и каждый элемент t∈s открыт, то пересечение ⋂₀ s открыто.

LaTeX

$$$\text{Finite } s \Rightarrow (\forall t\in s, IsOpen t) \Rightarrow IsOpen (\bigcap_{t\in s} t)$$$

Lean4

theorem isOpen_sInter {s : Set (Set X)} (hs : s.Finite) (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋂₀ s) := by
  induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)

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