English
Pull back a GeneralizedBooleanAlgebra along an injection: given f: α → β injective and maps preserving sup, inf, bottom and sdiff, α inherits a GeneralizedBooleanAlgebra structure via pullback from β.
Русский
Вытаскивание обобщенной булевой алгебры по инъекции: при задании инъекции f: α → β и отображений, сохраняющих ∫, ∠ и \, α получает структуру обобщенной булевой алгебры как вытянутая обратно структура β.
LaTeX
$$GeneralizedBooleanAlgebra α via pullback along f: α → β, with f injective and f(a \lor b) = f(a) \lor f(b), f(a \land b) = f(a) \land f(b), f(⊥) = ⊥, f(a \ b) = f(a) \ f(b)$$
Lean4
/-- Pullback a `GeneralizedBooleanAlgebra` along an injection. -/
protected abbrev generalizedBooleanAlgebra [Max α] [Min α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (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) : GeneralizedBooleanAlgebra α
where
__ := hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff
__ := hf.distribLattice f map_sup map_inf
sup_inf_sdiff a b := hf <| by rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
inf_inf_sdiff a
b :=
hf <| by
rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
-- See note [reducible non-instances]
