isOpen_source — Mathlib

English

Each source of a pretrivialization is open in the total space topology.

Русский

Каждый источник предтривиализации открыт в топологии полного пространства.

LaTeX

$$$ IsOpen\ a.totalSpaceTopology\ e.source $$$

Lean4

theorem isOpen_source (e : Pretrivialization F (π F E)) : IsOpen[a.totalSpaceTopology] e.source :=
  by
  refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_
  refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)
  ext ⟨x, hx⟩
  simp only [mem_preimage, Pretrivialization.setSymm, restrict, e.mem_target, e.mem_source, e'.proj_symm_apply hx]

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