tacticUnit_interval — Mathlib

English

projIcc(0,1,x) equals 0 if and only if x ≤ 0.

Русский

Проекция на [0,1] равна 0 тогда, когда x ≤ 0.

LaTeX

$$projIcc (0 : ℝ) 1 zero_le_one x = 0 \iff x ≤ 0$$

Lean4

/-- A tactic that solves `0 ≤ ↑x`, `0 ≤ 1 - ↑x`, `↑x ≤ 1`, and `1 - ↑x ≤ 1` for `x : I`. -/
@[tactic_parser 1000]
public meta def tacticUnit_interval : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Tactic.Interactive.tacticUnit_interval 1024 (ParserDescr.nonReservedSymbol✝ "unit_interval" false✝)

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