English
Given an injective map f: α → β and compatible maps preserving lattice and Boolean operations, α inherits a CompleteAtomicBooleanAlgebra structure from β.
Русский
При наличии инъекции f: α → β и подходящих отображений, сохраняющих операции объединения, пересечения и булеровских операций, α наследует структуру CompleteAtomicBooleanAlgebra от β.
LaTeX
$$CompleteAtomicBooleanAlgebra α$$
Lean4
/-- Pullback a `CompleteAtomicBooleanAlgebra` along an injection. -/
protected abbrev completeAtomicBooleanAlgebra [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α]
[HImp α] [HNot α] [SDiff α] [CompleteAtomicBooleanAlgebra β] (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_sSup : ∀ s, f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ s, f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤)
(map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b)
(map_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : CompleteAtomicBooleanAlgebra α
where
__ :=
hf.completelyDistribLattice f map_sup map_inf map_sSup map_sInf map_top map_bot map_compl map_himp map_hnot
map_sdiff
__ := hf.booleanAlgebra f map_sup map_inf map_top map_bot map_compl map_sdiff map_himp
