Equiv_isup_symm_inclusion — Mathlib

English

A reiteration of Equiv_iSup apply at a given i.

Русский

Повторение применения Equiv_iSup на указанном i.

LaTeX

$$$\\mathrm{Equiv\_iSup} S\\left(\\mathrm{of}_{L\\,\\iota\\,G\\ f\\ i} x\\right) = \\mathrm{Substructure.inclusion}(\\mathrm{le\\_iSup}\\ _ _) x.$$$

Lean4

@[simp]
theorem Equiv_isup_symm_inclusion (i : ι) :
    (Equiv_iSup S).symm.toEmbedding.comp (Substructure.inclusion (le_iSup _ _)) =
      of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i :=
  by ext x; exact Equiv_isup_symm_inclusion_apply _ x

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