sup_congr_left

Mathlib.Order.Lattice

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

English

If hb ≤ a ⊔ c and hc ≤ a ⊔ b, then a ⊔ b = a ⊔ c.

Русский

Если hb ≤ a ⊔ c и hc ≤ a ⊔ b, то a ⊔ b = a ⊔ c.

LaTeX

$$(hb \le a \sqcup c) ∧ (hc \le a \sqcup b) ⇒ a \sqcup b = a \sqcup c$$

Lean4

theorem sup_congr_left (hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) : a ⊔ b = a ⊔ c :=
  (sup_le le_sup_left hb).antisymm <| sup_le le_sup_left hc

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

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

Разделы

Аффилиация

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