bihimp_eq_bot — Mathlib

English

If a and b are complements, then bihimp(a,b) equals the bottom element; equivalently, a ⇔ b = ⊥ under an IsCompl relation.

Русский

Если a и b являются дополнениями, то bihimp(a,b) равно ⊥; эквивалентно a ⇔ b = ⊥ при IsCompl.

LaTeX

$$∀ {α} [HeytingAlgebra α] {a b : α}, IsCompl a b → bihimp a b = ⊥$$

Lean4

theorem bihimp_eq_bot {a b : α} (h : IsCompl a b) : a ⇔ b = ⊥ := by rw [h.eq_compl, compl_bihimp_self]

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