English
Pull back a Frame.MinimalAxioms along an injection: given minAx on β and a map f: α → β preserving ⊔, ⊓, sSup, sInf, top, bottom, the induced α carries Frame.MinimalAxioms.
Русский
Тянем назад Frame.MinimalAxioms вдоль инъекции: имея minAx на β и отображение f: α → β сохраняющее ⊔, ⊓, sSup, sInf, ⊤, ⊥, получаем Frame.MinimalAxioms на α.
LaTeX
$$$[Frame.MinimalAxioms\; \beta] \rightarrow \text{pullback along } f:\alpha \to \beta \Rightarrow Frame.MinimalAxioms(\alpha).$$$
Lean4
/-- Pullback an `Order.Frame.MinimalAxioms` along an injection. -/
protected abbrev frameMinimalAxioms [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α]
(minAx : Frame.MinimalAxioms β) (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 ⊥ = ⊥) : Frame.MinimalAxioms α
where
__ := hf.completeLattice f map_sup map_inf map_sSup map_sInf map_top map_bot
inf_sSup_le_iSup_inf a
s := by
change f (a ⊓ sSup s) ≤ f _
rw [← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]
simp_rw [← map_inf]
exact ((map_sSup _).trans iSup_image).ge
