Theorems · Theorem · order theory

GeneralizedHeytingAlgebra.le_himp_iff

∀ {α : Type u_4} [self : GeneralizedHeytingAlgebra α] (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c

(a ⇨ ·) is right adjoint to (a ⊓ ·)

Defined in

Mathlib.Order.Heyting.Basic

Cited by

1 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GeneralizedHeytingAlgebra