Ioo_mk_mk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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