exists_eq_top_of_iUnion_eq_univ — Mathlib

English

With finite index, the union of subspaces equalling the universal set implies a subspace is universal.

Русский

При конечном числе индексов объединение подпространств, равное вселенному, означает, что одно из подпространств вселенное.

LaTeX

$$$\exists i, p_i = \top$$$

Lean4

theorem exists_eq_top_of_iUnion_eq_univ {ι} [Finite ι] {p : ι → Subspace k E}
    (hcovers : ⋃ i, (p i : Set E) = Set.univ) : ∃ i, p i = ⊤ :=
  by
  have := Fintype.ofFinite (Set.range p)
  simp_rw [← Set.biUnion_range (f := p), ← Set.mem_toFinset] at hcovers
  apply Set.mem_toFinset.mp (Subspace.top_mem_of_biUnion_eq_univ hcovers)

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