coe_eq_coe_iff_of_mem_Ico — Mathlib

English

The equality expressing liftIoc as the composition of the restriction of f to Ico a (a+p) with the inverse of equivIco p a.

Русский

Равенство, выражающее liftIoc через композицию ограничения f на Ico a (a+p) с обратной функцией equivIco p a.

LaTeX

$$$$ \mathrm{liftIoc}(p,a,f) = \mathrm{Set.restrict}_{{\mathsf{Ico}}\ a\ (a+p)} f \circ (\mathrm{equivIoc}(p,a))^{-1} $$$$

Lean4

theorem coe_eq_coe_iff_of_mem_Ico {x y : 𝕜} (hx : x ∈ Ico a (a + p)) (hy : y ∈ Ico a (a + p)) :
    (x : AddCircle p) = y ↔ x = y := by
  refine ⟨fun h => ?_, by tauto⟩
  suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
  apply_fun equivIco p a at h
  rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
  exact h

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