sup_himp_self_left

Mathlib.Order.Heyting.Basic

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

English

For all a, b in α, (a ∨ b) → a = b → a.

Русский

Для любых a, b ∈ α верно (a ∨ b) ⇨ a = b ⇨ a.

LaTeX

$$$ a \lor b \to a = b \to a $$$

Lean4

@[simp]
theorem sup_himp_self_left (a b : α) : a ⊔ b ⇨ a = b ⇨ a := by rw [sup_himp_distrib, himp_self, top_inf_eq]

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

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

Разделы

Аффилиация

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