Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 18:24 98c61b1e

View on Github →

feat(order/hom/heyting): Heyting homomorphisms (#15308) Define the type of Heyting homomorphisms, maps between Heyting algebras that preserve Heyting implication.

Estimated changes

added theorem biheyting_hom.coe_comp
added theorem biheyting_hom.coe_id
added theorem biheyting_hom.comp_id
added theorem biheyting_hom.ext
added theorem biheyting_hom.id_apply
added theorem biheyting_hom.id_comp
added structure biheyting_hom
added theorem coheyting_hom.coe_comp
added theorem coheyting_hom.coe_id
added theorem coheyting_hom.comp_id
added theorem coheyting_hom.ext
added theorem coheyting_hom.id_apply
added theorem coheyting_hom.id_comp
added structure coheyting_hom
added theorem heyting_hom.coe_comp
added theorem heyting_hom.coe_id
added def heyting_hom.comp
added theorem heyting_hom.comp_apply
added theorem heyting_hom.comp_assoc
added theorem heyting_hom.comp_id
added theorem heyting_hom.ext
added theorem heyting_hom.id_apply
added theorem heyting_hom.id_comp
added structure heyting_hom
added theorem map_bihimp
added theorem map_compl
added theorem map_hnot
added theorem map_symm_diff
added theorem map_compl'
deleted theorem map_compl
added theorem map_sdiff'
deleted theorem map_sdiff
added theorem map_symm_diff'
deleted theorem map_symm_diff