English
Pull back a generalizedCoheytingAlgebra along an injection to obtain a generalizedCoheytingAlgebra structure on the domain, preserving sup, inf, bot, and difference.
Русский
Вытягивание по инъекции коейтинговой алгебры даёт структуру на области определения, сохраняющую операции sup, inf, bot и разность.
LaTeX
$$$\text{Function.Injective.generalizedCoheytingAlgebra}(f,hf,map\_sup,map\_inf,map\_bot,map\_sdiff) : \text{GeneralizedCoheytingAlgebra } \alpha$$$
Lean4
/-- Pullback a `GeneralizedCoheytingAlgebra` along an injection. -/
protected abbrev generalizedCoheytingAlgebra [Max α] [Min α] [Bot α] [SDiff α] [GeneralizedCoheytingAlgebra β]
(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_bot : f ⊥ = ⊥) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : GeneralizedCoheytingAlgebra α :=
{ __ := hf.lattice f map_sup map_inf
__ := ‹Bot α›
__ := ‹SDiff α›
bot_le := fun a => by
change f _ ≤ _
rw [map_bot]
exact bot_le,
sdiff_le_iff := fun a b c => by
change f _ ≤ _ ↔ f _ ≤ _
rw [map_sdiff, map_sup, sdiff_le_iff] }
-- See note [reducible non-instances]
