English
There is a bound relating the operator NN-norm of u to the finite basis, giving a bound in terms of the cardinal of index set and the basis norm.
Русский
Существует ограничение, связывающее норму оператора NN для u с базисом и размером индекса.
LaTeX
$$$ \|u\|_+ ≤ Fintype.card(ι) \cdot \|v.equivFunL.toContinuousLinearMap\|_+ \cdot M $$$
Lean4
theorem isOpen_setOf_affineIndependent {ι : Type*} [Finite ι] : IsOpen {p : ι → E | AffineIndependent 𝕜 p} := by
classical
rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
· exact isOpen_discrete _
· simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
let ι' := { x // x ≠ i₀ }
cases nonempty_fintype ι
haveI : Fintype ι' := Subtype.fintype _
convert_to IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
exact isOpen_setOf_linearIndependent.preimage (by fun_prop)
