two_mul_sub_one_mem_iff — Mathlib

English

For every real t, 2t − 1 belongs to the unit interval [0,1] if and only if t belongs to [1/2, 1].

Русский

Для каждого действительного t, 2t − 1 принадлежит отрезку [0,1], если и только если t принадлежит [1/2, 1].

LaTeX

$$$2 t - 1 \in [0,1] \iff t \in [\tfrac{1}{2}, 1]$$$

Lean4

theorem two_mul_sub_one_mem_iff {t : ℝ} : 2 * t - 1 ∈ I ↔ t ∈ Set.Icc (1 / 2 : ℝ) 1 := by
  constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor <;> linarith

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