bddBelow_projectiveSemiNormAux — Mathlib

English

The set { projectiveSeminormAux p.1 | p ∈ lifts x } is bounded below.

Русский

Множество { projectiveSeminormAux p.1 | p ∈ lifts x } ограничено снизу.

LaTeX

$$$ \\exists m\\in\\mathbb{R}, \\; m \\leq \\mathrm{projectiveSeminormAux}(p.1) \\text{ for all } p \\in \\mathrm{lifts}\, x $$$

Lean4

theorem bddBelow_projectiveSemiNormAux (x : ⨂[𝕜] i, E i) :
    BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) :=
  by
  existsi 0
  rw [mem_lowerBounds]
  simp only [Set.mem_range, Subtype.exists, exists_prop, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  exact fun p _ ↦ projectiveSeminormAux_nonneg p

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