sup_congr_right

Mathlib.Order.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem sup_congr_right (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c :=
  (sup_le ha le_sup_right).antisymm <| sup_le hb le_sup_right

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

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

Разделы

Аффилиация

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