qRight_zero_right — Mathlib

English

For t in I, qRight((t, 0)) equals 2t if t ≤ 1/2, and equals 1 otherwise.

Русский

Для t ∈ I выполнено: qRight((t,0)) = 2t, если t ≤ 1/2, иначе 1.

LaTeX

$$$qRight(t,0)=\begin{cases}2t,& t\le \tfrac12, \\ 1,& t>\tfrac12\end{cases}$ для всех $t\in I$$$

Lean4

theorem qRight_zero_right (t : I) : (qRight (t, 0) : ℝ) = if (t : ℝ) ≤ 1 / 2 then (2 : ℝ) * t else 1 :=
  by
  simp only [qRight, coe_zero, add_zero, div_one]
  split_ifs
  · rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]
    refine ⟨t.2.1, ?_⟩
    tauto
  · rw [(Set.projIcc_eq_right _).2]
    · linarith
    · exact zero_lt_one

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