English
Icc between two elements with the same first coordinate equals the image under Embedding.sigmaMk of the Icc in the fiber.
Русский
Icc между двумя элементами с одинаковой первой координатой равен образу под Embedding.sigmaMk i от Icc в волокне.
LaTeX
$$$\\mathrm{Icc} \\langle i,a\\rangle \\langle i,b\\rangle = \\mathrm{Finset}.map (\\mathrm{Embedding.sigmaMk } i) (\\mathrm{Icc} a b)$$$
Lean4
@[simp]
theorem Icc_mk_mk : Icc (⟨i, a⟩ : Sigma α) ⟨i, b⟩ = (Icc a b).map (Embedding.sigmaMk i) :=
dif_pos rfl