stolzSet_empty — Mathlib

English

If M ≤ 1, then stolzSet M is empty.

Русский

Если M ≤ 1, то stolzSet M пусто.

LaTeX

$$$ stolzSet M = \\emptyset \\, (\\text{when } M \\le 1)$$$

Lean4

theorem stolzSet_empty {M : ℝ} (hM : M ≤ 1) : stolzSet M = ∅ :=
  by
  ext z
  rw [stolzSet, Set.mem_setOf, Set.mem_empty_iff_false, iff_false, not_and, not_lt, ← sub_pos]
  intro zn
  calc
    _ ≤ 1 * (1 - ‖z‖) := mul_le_mul_of_nonneg_right hM zn.le
    _ = ‖(1 : ℂ)‖ - ‖z‖ := by rw [one_mul, norm_one]
    _ ≤ _ := norm_sub_norm_le _ _

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