projIci_coe — Mathlib

English

Let α be a linearly ordered set and a ∈ α. Then for every x with a ≤ x, the projection onto Ici a fixes x: projIci a x = x.

Русский

Пусть α линейно упорядочено, и a ∈ α. Тогда для каждого x с a ≤ x проекция на Ici a возвращает сам x: projIci a x = x.

LaTeX

$$$\forall x \in [a, \infty),\; \operatorname{projIci}(a)(x) = x$$$

Lean4

@[simp]
theorem projIci_coe (x : Ici a) : projIci a x = x := by cases x; apply projIci_of_mem

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