Ico_mk_mk — Mathlib

English

Ico between two elements with the same first coordinate equals the fiber Ico mapped by Embedding.sigmaMk.

Русский

Ico между двумя элементами с одинаковой первой координатой равен образу Ico в волокне под Embedding.sigmaMk.

LaTeX

$$$\\mathrm{Ico} \\langle i,a\\rangle \\langle i,b\\rangle = \\mathrm{Finset}.map (\\mathrm{Embedding.sigmaMk } i) (\\mathrm{Ico} a b)$$$

Lean4

@[simp]
theorem Ico_mk_mk : Ico (⟨i, a⟩ : Sigma α) ⟨i, b⟩ = (Ico a b).map (Embedding.sigmaMk i) :=
  dif_pos rfl

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