balancedCoreAux_balanced — Mathlib

English

balancedCoreAux 𝕜 s is balanced.

Русский

balancedCoreAux 𝕜 s является сбалансированным множеством.

LaTeX

$$Balanced\\ 𝕜\\ (balancedCoreAux\\ 𝕜\\ s)$$

Lean4

theorem balancedCoreAux_balanced (h0 : (0 : E) ∈ balancedCoreAux 𝕜 s) : Balanced 𝕜 (balancedCoreAux 𝕜 s) :=
  by
  rintro a ha x ⟨y, hy, rfl⟩
  obtain rfl | h := eq_or_ne a 0
  · simp_rw [zero_smul, h0]
  rw [mem_balancedCoreAux_iff] at hy ⊢
  intro r hr
  have h'' : 1 ≤ ‖a⁻¹ • r‖ := by
    rw [norm_smul, norm_inv]
    exact one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr
  have h' := hy (a⁻¹ • r) h''
  rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'

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