isOpen_iff_inter — Mathlib

English

For an open cover U, a set s is open iff each preimage under the canonical inclusion to U i is open.

Русский

Для открытого покрытия U множество s открыто тогда и только тогда, когда прообраз через включение в каждое U i будет открытым.

LaTeX

$$$IsOpen s \\iff \\forall i, IsOpen ((↑)^{-1}' s : Set (U i))$$$

Lean4

theorem isOpen_iff_inter : IsOpen s ↔ ∀ i, IsOpen (s ∩ U i) :=
  by
  constructor
  · exact fun H i ↦ H.inter (U i).isOpen
  · intro H
    simpa [← inter_iUnion, hU.iSup_set_eq_univ] using isOpen_iUnion H

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