isOpen_setOf_nat_le_rank — Mathlib

English

For any natural number n, the set of linear maps with rank at least n is open.

Русский

Для любого натурального числа n множество отображений с рангом не меньше n открыто.

LaTeX

$$$\{f: E \to_L F \mid \mathrm{rank}(f) \ge n\}$ is open$$

Lean4

theorem isOpen_setOf_nat_le_rank (n : ℕ) : IsOpen {f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank} :=
  by
  simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]
  refine isOpen_biUnion fun t _ => ?_
  have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
    continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
  exact isOpen_setOf_linearIndependent.preimage this

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