balancedCore — Mathlib

English

If 0 ∈ s, balancedCore 𝕜 s equals the intersection over all r with 1≤‖r‖ of r•s.

Русский

Если 0 ∈ s, то balancedCore 𝕜 s равно пересечению по всем r, для которых 1≤‖r‖, множества r•s.

LaTeX

$$If\\ 0 \\in s\\ then\\ balancedCore\\ 𝕜\\ s = \\bigcap_{r:𝕜,\ 1\\le \\|r\\|} (r\\cdot s)$$

Lean4

protected theorem balancedCore (hU : IsClosed U) : IsClosed (balancedCore 𝕜 U) :=
  by
  by_cases h : (0 : E) ∈ U
  · rw [balancedCore_eq_iInter h]
    refine isClosed_iInter fun a => ?_
    refine isClosed_iInter fun ha => ?_
    have ha' := lt_of_lt_of_le zero_lt_one ha
    rw [norm_pos_iff] at ha'
    exact isClosedMap_smul_of_ne_zero ha' U hU
  · have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
    rw [this]
    exact isClosed_empty

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