isOpen_iff_coe_preimage — Mathlib

English

In a TopologicalSpace with an open cover U, IsOpen s is equivalent to IsOpen of each preimage under the canonical inclusions.

Русский

В топологическом пространстве с открытым покрытием U, равносильно: IsOpen s эквивалентно IsOpen каждого прообраза через канонические включения.

LaTeX

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

Lean4

theorem isOpen_iff_coe_preimage : IsOpen s ↔ ∀ i, IsOpen ((↑) ⁻¹' s : Set (U i)) := by
  simp [hU.isOpen_iff_inter (s := s), (U _).2.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
    image_preimage_eq_inter_range]

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