balancedCoreAux — Mathlib

English

Characterizes membership in balancedCore: x ∈ balancedCore 𝕜 s iff there exists a balanced t ⊆ s with x ∈ t.

Русский

Характеризуется принадлежность: x ∈ balancedCore 𝕜 s эквивалентно существованию сбалансированного t ⊆ s с x ∈ t.

LaTeX

$$$x \\in balancedCore 𝕜 s \\iff \\exists t, Balanced 𝕜 t \\land t \\subseteq s \\land x \\in t$$$

Lean4

/-- Helper definition to prove `balanced_core_eq_iInter` -/
def balancedCoreAux (s : Set E) :=
  ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s

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