le_inf

Mathlib.CategoryTheory.Subobject.Lattice

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

← MathLib Explorer

English

If h ≤ f and h ≤ g, then h ≤ (inf.obj f).obj g.

Русский

Если h ≤ f и h ≤ g, то h ≤ (inf.obj f).obj g.

LaTeX

$$$ h \\le f \\land h \\le g \\Longrightarrow h \\le (\\inf.obj f).obj g $$$

Lean4

theorem le_inf {A : C} (h f g : Subobject A) : h ≤ f → h ≤ g → h ≤ (inf.obj f).obj g :=
  Quotient.inductionOn₃' h f g
    (by
      rintro f g h ⟨k⟩ ⟨l⟩
      exact ⟨MonoOver.leInf _ _ _ k l⟩)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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