subset_balancedCore — Mathlib

English

If 0 ∈ t and for all a with ‖a‖≤1 we have a•s ⊆ t, then s ⊆ balancedCore 𝕜 t.

Русский

Пусть 0 ∈ t и для всех a с ‖a‖≤1 выполнено a•s ⊆ t; тогда s ⊆ balancedCore 𝕜 t.

LaTeX

$$(ht : 0 \\in t) \\land (hst : ∀ a:𝕜, \\|a\\| ≤ 1 → a\\cdot s ⊆ t) ⇒ s ⊆ balancedCore 𝕜 t$$

Lean4

theorem subset_balancedCore (ht : (0 : E) ∈ t) (hst : ∀ a : 𝕜, ‖a‖ ≤ 1 → a • s ⊆ t) : s ⊆ balancedCore 𝕜 t :=
  by
  rw [balancedCore_eq_iInter ht]
  refine subset_iInter₂ fun a ha ↦ ?_
  rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]
  apply hst
  rw [norm_inv]
  exact inv_le_one_of_one_le₀ ha

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