apply_mk

Mathlib.Topology.Category.TopCat.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.apply_mk

English

Given a morphism f: U → V and a point x ∈ X, the image of ⟨x, hx⟩ under f is ⟨x, f.le hx⟩.

Русский

Пусть f: U → V и x ∈ X, тогда f⟨x, hx⟩ = ⟨x, f.le hx⟩.

LaTeX

$$$f(\langle x, hx \rangle) = \langle x, f.le hx \rangle$$$

Lean4

@[simp]
theorem apply_mk (f : U ⟶ V) (x : X) (hx) : f ⟨x, hx⟩ = ⟨x, f.le hx⟩ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru