sup_eq_sup_iff_right

Mathlib.Order.Lattice

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem sup_eq_sup_iff_right : a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c :=
  ⟨fun h => ⟨h ▸ le_sup_left, h.symm ▸ le_sup_left⟩, fun h => sup_congr_right h.1 h.2⟩

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

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

Разделы

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

Аффилиация

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