Icc_mk_mk — Mathlib

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

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