lt_sup_iff

Mathlib.Order.Lattice

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

← MathLib Explorer

English

In a linear order, a < b ⊔ c iff a < b or a < c.

Русский

В линейном порядке a < b ∨ c эквивалентно a < b или a < c.

LaTeX

$$$a < b \vee c \iff a < b \lor a < c$$$

Lean4

@[simp]
theorem lt_sup_iff : a < b ⊔ c ↔ a < b ∨ a < c := by
  exact
    ⟨fun h => (le_total c b).imp (fun bc => by rwa [sup_eq_left.2 bc] at h) (fun bc => by rwa [sup_eq_right.2 bc] at h),
      fun h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩

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

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

Разделы

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

Аффилиация

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