iSup_iInf_eq — Mathlib

English

The product of a family of Coframes is again a Coframe: if each π(i) is a Coframe, then the product (i → π(i)) is a Coframe.

Русский

Произведение семейства Coframe снова является Coframe: если каждый π(i) — Coframe, то произведение (i → π(i)) — Coframe.

LaTeX

$$Coframe((i : ι) → π i)$$

Lean4

theorem iSup_iInf_eq [CompletelyDistribLattice α] {f : ∀ a, κ a → α} :
    (⨆ a, ⨅ b, f a b) = ⨅ g : ∀ a, κ a, ⨆ a, f a (g a) :=
  CompletelyDistribLattice.MinimalAxioms.of.iSup_iInf_eq _

Похожие утверждения