of_subsingleton — Mathlib

English

If E is a singleton, every subset is von Neumann bounded.

Русский

Если множество состоит из одного элемента, любое подмножество VonNBounded.

LaTeX

$$$[Subsingleton E] \Rightarrow IsVonNBounded 𝕜 s$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton E] {s : Set E} : IsVonNBounded 𝕜 s := fun U hU ↦
  .of_forall fun c ↦
    calc
      s ⊆ univ := subset_univ s
      _ = c • U := .symm <| Subsingleton.eq_univ_of_nonempty <| (Filter.nonempty_of_mem hU).image _

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