projIci — Mathlib

English

Projection to the closed upper interval [a, ∞) in α, sending x to (max(a, x), proof of a ≤ max(a, x)).

Русский

Проекция на замкнутый интервал [a, ∞) в α, отображающая x в (max(a, x), доказательство a ≤ max(a, x)).

LaTeX

$$projIci(a,x) = ⟨max(a,x), le_max_left(a,x)⟩.$$

Lean4

/-- Projection of `α` to the closed interval `[a, ∞)`. -/
def projIci (a x : α) : Ici a :=
  ⟨max a x, le_max_left _ _⟩

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