English
Pull back CompletelyDistribLattice.MinimalAxioms along an injection; the result satisfies the required equalities involving iInf, iSup and lattice operations.
Русский
Тянуть назад CompletelyDistribLattice.MinimalAxioms вдоль инъекции; результат удовлетворяет требуемым равенствам по iInf, iSup и операциям решётки.
LaTeX
$$$[CompletelyDistribLattice.MinimalAxioms\; \beta] \rightarrow \text{pullback along } f:\alpha \to \beta \Rightarrow CompletelyDistribLattice.MinimalAxioms(\alpha).$$$
Lean4
/-- Pullback a `CompletelyDistribLattice.MinimalAxioms` along an injection. -/
protected abbrev completelyDistribLatticeMinimalAxioms [Max α] [Min α] [SupSet α] [InfSet α] [Top α] [Bot α]
(minAx : CompletelyDistribLattice.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 ⊥ = ⊥) :
CompletelyDistribLattice.MinimalAxioms α
where
__ :=
hf.completeDistribLatticeMinimalAxioms minAx.toCompleteDistribLattice f map_sup map_inf map_sSup map_sInf map_top
map_bot
iInf_iSup_eq
g :=
hf <| by
simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range, minAx.iInf_iSup_eq']
-- See note [reducible non-instances]
