finset_sup_apply_lt — Mathlib

English

Scaling the infimum of two seminorms by a scalar respects infimum: r • (p ⊓ q) = (r • p) ⊓ (r • q).

Русский

Умножение на скаляр инфимума двух семинорм сохраняет минимум: r•(p ⊓ q) = (r•p) ⊓ (r•q).

LaTeX

$$$r \cdot (p \square q) = (r \cdot p) \square (r \cdot q)$$$

Lean4

theorem finset_sup_apply_lt {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 < a)
    (h : ∀ i, i ∈ s → p i x < a) : s.sup p x < a :=
  by
  lift a to ℝ≥0 using ha.le
  rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]
  · exact h
  · exact NNReal.coe_pos.mpr ha

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