bihimp_eq_sup_himp_inf — Mathlib

English

The bihimp of a and b equals the implication from the supremum to the infimum, i.e., bihimp(a,b) = himp(a ⊔ b, a ⊓ b).

Русский

Бихимп пары a и b равен импликации от их верховой границы к их нижней границе: bihimp(a,b) = himp(a ⊔ b, a ⊓ b).

LaTeX

$$$\bihimp(a,b) = \operatorname{himp}(a \vee b, a \wedge b)$$$

Lean4

theorem bihimp_eq_sup_himp_inf : a ⇔ b = a ⊔ b ⇨ a ⊓ b := by simp [himp_inf_distrib, bihimp]

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