mul_pos_mem_iff — Mathlib

English

Let a > 0. Then a·t lies in the unit interval [0,1] if and only if t lies in the closed interval [0, 1/a].

Русский

Пусть a > 0. Тогда a·t принадлежит отрезку [0,1] тогда и только тогда, когда t принадлежит отрезку [0,1/a].

LaTeX

$$$0 < a \implies (a t \in [0,1] \iff t \in [0,\tfrac{1}{a}])$$$

Lean4

theorem mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) : a * t ∈ I ↔ t ∈ Set.Icc (0 : ℝ) (1 / a) :=
  by
  constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor
  · exact nonneg_of_mul_nonneg_right h₁ ha
  · rwa [le_div_iff₀ ha, mul_comm]
  · exact mul_nonneg ha.le h₁
  · rwa [le_div_iff₀ ha, mul_comm] at h₂

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