sup_eq_sup_iff_left

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#sup_eq_sup_iff_left

← MathLib Explorer

English

a ⊔ b = a ⊔ c iff b ≤ a ⊔ c and c ≤ a ⊔ b.

Русский

a ⊔ b = a ⊔ c тогда и только тогда, когда b ≤ a ⊔ c и c ≤ a ⊔ b.

LaTeX

$$$a \sqcup b = a \sqcup c \iff b \le a \sqcup c \land c \le a \sqcup b$$$

Lean4

theorem sup_eq_sup_iff_left : a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b :=
  ⟨fun h => ⟨h ▸ le_sup_right, h.symm ▸ le_sup_right⟩, fun h => sup_congr_left h.1 h.2⟩

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

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

Разделы

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

Аффилиация

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