inf_lt_iff

Mathlib.Order.Lattice

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

English

In a linear order α, b ∧ c < a if and only if b < a or c < a.

Русский

В линейном порядке α, b ⊓ c < a тогда и только тогда, когда b < a или c < a.

LaTeX

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

Lean4

@[simp]
theorem inf_lt_iff : b ⊓ c < a ↔ b < a ∨ c < a :=
  @lt_sup_iff αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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