projIic_coe — Mathlib

English

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

Русский

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

LaTeX

$$$\forall x \in (-\infty, b],\; \operatorname{projIic}(b)(x) = x$$$

Lean4

@[simp]
theorem projIic_coe (x : Iic b) : projIic b x = x := by cases x; apply projIic_of_mem

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