isEquiv_iff_lt_one_iff — Mathlib

English

Equivalence of v and w is equivalent to the property that for all x, v(x) < 1 iff w(x) < 1.

Русский

Эквивалентность v и w эквивалентна свойству: для всех x, v(x) < 1 тогда и только тогда, когда w(x) < 1.

LaTeX

$$$ (v \sim w) \iff (\forall x,\ v(x) < 1 \iff w(x) < 1)$$$

Lean4

theorem isEquiv_iff_lt_one_iff : v.IsEquiv w ↔ ∀ x, v x < 1 ↔ w x < 1 :=
  by
  refine ⟨fun h _ ↦ h.lt_one_iff, fun h x y ↦ ?_⟩
  rcases eq_or_ne (v x) 0 with (_ | hy₀) <;> simp_all
  rw [le_iff_le_iff_lt_iff_lt, ← one_mul (v x), ← mul_inv_lt_iff₀ (by simp_all), ← one_mul (w x), ←
    mul_inv_lt_iff₀ (by simp_all), ← map_inv₀, ← map_mul, ← map_inv₀, ← map_mul]
  exact h _

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