instFunLike — Mathlib

English

For a morphism f: U → V in OpenNhds x and an element y ∈ U, the action of f on y preserves the underlying point, i.e., f(y) = y in the ambient space.

Русский

Для морфизма f: U → V в OpenNhds x и элемента y ∈ U, действие f на y сохраняет точку: f(y) = y в окружающем пространстве.

LaTeX

$$$f(\\langle y,\\, \\text{hy} \\rangle)=\\langle y,\\, f\\\\le \\text{hy} \\rangle$$$

Lean4

instance instFunLike : FunLike (U ⟶ V) U.1 V.1
    where
  coe f := Set.inclusion f.le
  coe_injective' := by rintro ⟨⟨_⟩⟩ _ _; congr!

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