piIso — Mathlib

English

There is an order isomorphism between the space of monotone maps α →o ∀ i, π i and the space ∀ i, α →o π i.

Русский

Существует изоморфизм порядка между пространством монотонных отображений α →o ∀ i, π i и пространством ∀ i, α →o π i.

LaTeX

$$$ piIso : (α \to^o ∀ i, π i) \cong^o ∀ i, α \to^o π i $$$

Lean4

/-- Order isomorphism between bundled monotone maps `α →o Π i, π i` and families of bundled monotone
maps `Π i, α →o π i`. -/
@[simps]
def piIso : (α →o ∀ i, π i) ≃o ∀ i, α →o π i
    where
  toFun f i := (Pi.evalOrderHom i).comp f
  invFun := pi
  map_rel_iff' := forall_swap

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