English
Similarly, the quotient description using IocMod coincides with the lift through the endpoint-identification, reflecting the Ioc interval as a canonical representative.
Русский
Аналогично, описание по факторгруппе через IocMod совпадает с поднятием через идентификацию концов, что отражает интервал Ioc как канонический представитель.
LaTeX
$$$$ \\text{equivIccQuot}(p,a) \\circ \\operatorname{Quotient.mk}'' = \\operatorname{Quot}(\\_, \\langle toIocMod(\\,hp.out\\, a \\,, x), \\_ \\rangle) $$$$
Lean4
theorem equivIccQuot_comp_mk_eq_toIocMod :
equivIccQuot p a ∘ Quotient.mk'' = fun x =>
Quot.mk _ ⟨toIocMod hp.out a x, Ioc_subset_Icc_self <| toIocMod_mem_Ioc _ _ x⟩ :=
by
rw [equivIccQuot_comp_mk_eq_toIcoMod]
funext x
by_cases h : a ≡ x [PMOD p]
· simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
exact Quot.sound EndpointIdent.mk
· simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]
