le₁₃

Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

URI: https://scilib.ai/kg/mathlib#Lattice.BicartSq.le₁₃

English

In a lattice with a bicartesian square, x1 ≤ x3 holds.

Русский

В решетке с би-картезианским квадратом выполняется x1 ≤ x3.

LaTeX

$$$x_1 \\le x_3$$$

Lean4

theorem le₁₃ : x₁ ≤ x₃ := by grind

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

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

Разделы

Аффилиация

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