le_sup

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#SupPrime.le_sup

English

If a is SupPrime, then a ≤ b ⊔ c iff a ≤ b or a ≤ c.

Русский

Если a — SupPrime, то a ≤ b ⊔ c эквивалентно a ≤ b или a ≤ c.

LaTeX

$$SupPrime\ a \rightarrow (a \le b \lor a \le c) \iff a \le b \lor a \le c$$

Lean4

theorem le_sup (ha : SupPrime a) : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c :=
  ⟨fun h => ha.2 h, fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩

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

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

Разделы

Аффилиация

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