projIic — Mathlib

English

Projection to the closed lower interval (−∞, b], mapping x to (min(b, x), proof of x ≥ min(b, x)).

Русский

Проекция на закрытый интервал (−∞, b], отображающая x в (min(b, x), доказательство x ≥ min(b, x)).

LaTeX

$$projIic(b,x) = ⟨min(b,x), min_le_left(b,x)⟩.$$

Lean4

/-- Projection of `α` to the closed interval `(-∞, b]`. -/
def projIic (b x : α) : Iic b :=
  ⟨min b x, min_le_left _ _⟩

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