map_top

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.map_top

English

See 81560: the map-top formula for mono morphisms.

Русский

См. 81560: формула отображения на вершину для монострого.

LaTeX

$$$(\text{map } f).\text{obj }\top = \operatorname{Subobject}.mk f$$$

Lean4

@[simp]
theorem map_top (f : X ⟶ Y) [Mono f] : (map f).obj ⊤ = Subobject.mk f :=
  Quotient.sound' ⟨MonoOver.mapTop f⟩

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

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

Разделы

Аффилиация

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