piLTLim_symm_apply — Mathlib

English

The symmetry of the equivalence piLTLim yields a formula for applying its inverse to an appropriate element.

Русский

Симметрия эквиваленции piLTLim даёт формулу применения её обратного к соответствующему элементу.

LaTeX

$$$(\\mathrm{piLTLim}(hi)).symm\\; f\\; l = f.1 k \\langle l, hl \\rangle$$$

Lean4

theorem piLTLim_symm_apply {f} (k : Iio i) {l : Iio i} (hl : l.1 < k.1) :
    (piLTLim (X := X) hi).symm f l = f.1 k ⟨l, hl⟩ :=
  by
  conv_rhs => rw [← (piLTLim hi).right_inv f]
  rfl

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