isOpen_setOf_linearIndependent — Mathlib

English

The set of injective continuous linear maps is open when E is finite-dimensional.

Русский

Множество инъективных непрерывных линейных отображений открыто, если E конечномерно.

LaTeX

$$$\text{IsOpen} \{L: E\to F \mid Injective L\}$$$

Lean4

theorem isOpen_setOf_linearIndependent {ι : Type*} [Finite ι] : IsOpen {f : ι → E | LinearIndependent 𝕜 f} :=
  isOpen_iff_mem_nhds.2 fun _ => LinearIndependent.eventually

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