map_eq — Mathlib

English

If two morphisms f and g between topological spaces X ⟶ Y are equal, then the induced mappings on open sets are equal; i.e., mapping of f equals mapping of g whenever f = g.

Русский

Если два морфизма f и g между топологическими пространствами X ⟶ Y равны, то индуцируемые отображения между открытымимножествами совпадают; то есть map(f) = map(g) при f = g.

LaTeX

$$$\forall X,Y\,\forall f,g: X\to Y,\, h: f=g \Rightarrow \mathrm{map}(f)=\mathrm{map}(g).$$$

Lean4

theorem map_eq (f g : X ⟶ Y) (h : f = g) : map f = map g :=
  by
  subst h
  rfl

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