himp_eq_left

Mathlib.Order.BooleanAlgebra.Basic

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

English

In a Boolean algebra, x ⇨ y = x iff x = ⊤ and y = ⊤.

Русский

В булевой алгебре x ⇨ y = x эквивалентно x = ⊤ и y = ⊤.

LaTeX

$$x \Rightarrow y = x \iff x = \top \land y = \top$$

Lean4

@[simp]
theorem himp_eq_left : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤ := by rw [codisjoint_himp_self_left.eq_iff]; aesop

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

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

Разделы

Аффилиация

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