English
Pull back a BiheytingAlgebra along an injection to obtain a BiheytingAlgebra on the domain, preserving both Heyting and Coheyting structures.
Русский
Вытягивание по инъекции для би-ейтинговой алгебры даёт биейтинговую структуру на области определения.
LaTeX
$$$\text{Function.Injective.biheytingAlgebra}(f,hf,map\_sup,map\_inf,map\_top,map\_bot,map\_compl,map\_hnot,map\_himp,map\_sdiff) : \text{BiheytingAlgebra } \alpha$$$
Lean4
/-- Pullback a `BiheytingAlgebra` along an injection. -/
protected abbrev biheytingAlgebra [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [HNot α] [HImp α] [SDiff α]
[BiheytingAlgebra β] (f : α → β) (hf : Injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
(map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
(map_hnot : ∀ a, f (￢a) = ￢f a) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
(map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : BiheytingAlgebra α :=
{ hf.heytingAlgebra f map_sup map_inf map_top map_bot map_compl map_himp,
hf.coheytingAlgebra f map_sup map_inf map_top map_bot map_hnot map_sdiff with }
