eq_top_mono

Mathlib.Order.BoundedOrder.Basic

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

English

If a ≤ b and a = ⊤, then b = ⊤.

Русский

Если a ≤ b и a = ⊤, то b = ⊤.

LaTeX

$$$(a \le b) \land (a = \top) \Rightarrow b = \top$$$

Lean4

theorem eq_top_mono (h : a ≤ b) (h₂ : a = ⊤) : b = ⊤ :=
  top_unique <| h₂ ▸ h

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

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

Разделы

Аффилиация

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