English
Pullback of a Coframe.MinimalAxioms along an injection to α yields a Coframe.MinimalAxioms on α.
Русский
Тянем назад Coframe.MinimalAxioms по инъекции на α, получаем Coframe.MinimalAxioms на α.
LaTeX
$$$\text{Coframe.MinimalAxioms}(\alpha).$$$
Lean4
/-- Pullback an `Order.Frame` along an injection. -/
protected abbrev frame [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HasCompl α] [HImp α] [Frame β] (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) : Frame α
where
__ := hf.frameMinimalAxioms .of f map_sup map_inf map_sSup map_sInf map_top map_bot
__ := hf.heytingAlgebra f map_sup map_inf map_top map_bot map_compl map_himp
