Theorems · Theorem · order theory

BiheytingHomClass.map_himp

∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : BiheytingHomClass F α β] (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b

The proposition that a bi-Heyting homomorphism preserves the Heyting implication.

Defined in

Mathlib.Order.Heyting.Hom

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

BiheytingHomClass