balancedCoreAux_maximal — Mathlib

English

If t ⊆ s and Balanced 𝕜 t, then t ⊆ balancedCoreAux 𝕜 s.

Русский

Если t ⊆ s и t сбалансировано, то t ⊆ balancedCoreAux 𝕜 s.

LaTeX

$$(t ⊆ s) ∧ Balanced\\ 𝕜\\ t \\Rightarrow t ⊆ balancedCoreAux\\ 𝕜\\ s$$

Lean4

theorem balancedCoreAux_maximal (h : t ⊆ s) (ht : Balanced 𝕜 t) : t ⊆ balancedCoreAux 𝕜 s :=
  by
  refine fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_
  rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]
  refine h (ht.smul_mem ?_ hx)
  rw [norm_inv]
  exact inv_le_one_of_one_le₀ hr

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