Ioc_mk_mk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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