isOpen_iff — Mathlib

English

A subset U of the glued carrier is open iff all its preimages under the injections ι_i are open.

Русский

Подмножество U склеенного носителя открыто тогда и только тогда, когда все его предобразные по инъекциям ι_i открыты.

LaTeX

$$$\text{IsOpen}(U) \iff \forall i,\; \text{IsOpen}( (D.\ι i)^{\text{base}^{-1}}(U) )$$$

Lean4

theorem isOpen_iff (U : Set D.glued.carrier) : IsOpen U ↔ ∀ i, IsOpen ((D.ι i).base ⁻¹' U) :=
  by
  rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage, TopCat.GlueData.isOpen_iff]
  apply forall_congr'
  intro i
  rw [← Set.preimage_comp, ← ι_isoCarrier_inv]
  rfl

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