map_homOfLE — Mathlib

English

For any map f, the image of the top open set is the top open set: (Opens.map f).obj ⊤ = ⊤.

Русский

Для любого отображения f изображение верхнего открытого множества является верхним открытым множеством: (Opens.map f).obj ⊤ = ⊤.

LaTeX

$$$(\\mathrm{Opens.map}\\ f).\\mathrm{obj} \\top = \\top$$$

Lean4

@[simp]
theorem map_homOfLE (f : X ⟶ Y) {U V : Opens Y} (e : U ≤ V) :
    (TopologicalSpace.Opens.map f).map (homOfLE e) =
      homOfLE (show (Opens.map f).obj U ≤ (Opens.map f).obj V from fun _ hx ↦ e hx) :=
  rfl

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