English
Pull back a HeytingAlgebra along an injection to obtain a HeytingAlgebra structure on the domain, preserving top, bottom, complement, and implication.
Русский
Вытягивание по инъекции для хейтинговой алгебры даёт структуру на области определения, сохраняющую ⊤, ⊥, комплемент и импликацию.
LaTeX
$$$\text{Function.Injective.heytingAlgebra}(f,hf,map\_sup,map\_inf,map\_top,map\_bot,map\_compl,map\_himp) : \text{HeytingAlgebra } \alpha$$$
Lean4
/-- Pullback a `HeytingAlgebra` along an injection. -/
protected abbrev heytingAlgebra [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [HImp α] [HeytingAlgebra β] (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_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) :
HeytingAlgebra α :=
{ __ := hf.generalizedHeytingAlgebra f map_sup map_inf map_top map_himp
__ := ‹Bot α›
__ := ‹HasCompl α›
bot_le := fun a => by
change f _ ≤ _
rw [map_bot]
exact bot_le,
himp_bot := fun a => hf <| by rw [map_himp, map_compl, map_bot, himp_bot] }
-- See note [reducible non-instances]
