English
Pull back a Coframe along an injection from α to β, obtaining a Coframe on α with preserved operations.
Русский
Тянем назад Coframe вдоль инъекции из α в β, получаем Coframe на α с сохранёнными операциями.
LaTeX
$$$[Max α][Min α][SupSet α][InfSet α][Top α][Bot α] \rightarrow Coframe(\alpha)$ по инъекции сохраняющее операции.$$
Lean4
/-- Pullback an `Order.Coframe` along an injection. -/
protected abbrev coframe [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α] [HNot α] [SDiff α] [Coframe β]
(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_hnot : ∀ a, f (￢a) = ￢f a) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) : Coframe α
where
__ := hf.coframeMinimalAxioms .of f map_sup map_inf map_sSup map_sInf map_top map_bot
__ := hf.coheytingAlgebra f map_sup map_inf map_top map_bot map_hnot map_sdiff
