exists_finiteIndex_of_cover — Mathlib

English

A finite union of proper subspaces of a vector space over an infinite field cannot cover the entire space.

Русский

Конечное объединение неполных подпространств не покрывает всю пространство над бесконечным телом.

LaTeX

$$$\bigcup_{p \in s} (p : Set E) \neq \operatorname{Set.univ}$$$

Lean4

theorem exists_finiteIndex_of_cover (hcovers : ⋃ i ∈ s, (p i : Set M) = Set.univ) :
    ∃ k ∈ s, (p k).toAddSubgroup.FiniteIndex :=
  have hcovers' : ⋃ i ∈ s, (0 : M) +ᵥ ((p i).toAddSubgroup : Set M) = Set.univ := by
    simpa only [zero_vadd] using hcovers
  AddSubgroup.exists_finiteIndex_of_leftCoset_cover hcovers'

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