isOpen_iff_of_cover — Mathlib

English

Let f_i be an open cover of X. Then s is open iff each intersection f_i ∩ s is open.

Русский

Пусть {f_i} является открытым покрытием X. Тогда s открыто тогда и только тогда, когда каждый f_i ∩ s открыт.

LaTeX

$$$\IsOpen(s) \iff \forall i, IsOpen (f_i \cap s)$$$

Lean4

theorem isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) :
    IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) :=
  by
  refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
  rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
  exact isOpen_iUnion fun i ↦ h i

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