English
Pull back CompletelyDistribLattice.MinimalAxioms along an injection, yielding a CompletelyDistribLattice.MinimalAxioms on α.
Русский
Тянем назад CompletelyDistribLattice.MinimalAxioms вдоль инъекции, получаем CompletelyDistribLattice.MinimalAxioms на α.
LaTeX
$$$[CompletelyDistribLattice.MinimalAxioms\; \beta] \rightarrow \text{pullback along } f:\alpha \to \beta \Rightarrow CompletelyDistribLattice.MinimalAxioms(\alpha).$$$
Lean4
/-- Pullback a `CompleteDistribLattice.MinimalAxioms` along an injection. -/
protected abbrev completeDistribLatticeMinimalAxioms [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α]
(minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β) (hf : Injective f)
(map_sup :
let _ := minAx.toCompleteLattice
∀ a b, f (a ⊔ b) = f a ⊔ f b)
(map_inf :
let _ := minAx.toCompleteLattice
∀ a b, f (a ⊓ b) = f a ⊓ f b)
(map_sSup :
let _ := minAx.toCompleteLattice
∀ s, f (sSup s) = ⨆ a ∈ s, f a)
(map_sInf :
let _ := minAx.toCompleteLattice
∀ s, f (sInf s) = ⨅ a ∈ s, f a)
(map_top :
let _ := minAx.toCompleteLattice
f ⊤ = ⊤)
(map_bot :
let _ := minAx.toCompleteLattice
f ⊥ = ⊥) :
CompleteDistribLattice.MinimalAxioms α
where
__ := hf.frameMinimalAxioms minAx.toFrame f map_sup map_inf map_sSup map_sInf map_top map_bot
__ := hf.coframeMinimalAxioms minAx.toCoframe f map_sup map_inf map_sSup map_sInf map_top map_bot
