balancedCore_nonempty_iff — Mathlib

English

The balanced core of s is nonempty if and only if 0 ∈ s.

Русский

Сбалансированное ядро множества s непусто тогда и только тогда, когда 0 ∈ s.

LaTeX

$$$(balancedCore 𝕜\\ s).Nonempty \\iff 0 \\in s$$$

Lean4

theorem balancedCore_nonempty_iff : (balancedCore 𝕜 s).Nonempty ↔ (0 : E) ∈ s :=
  ⟨fun h =>
    zero_subset.1 <|
      (zero_smul_set h).superset.trans <|
        (balancedCore_balanced s (0 : 𝕜) <| norm_zero.trans_le zero_le_one).trans <| balancedCore_subset _,
    fun h => ⟨0, balancedCore_zero_mem h⟩⟩

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