biUnion_ne_univ_of_top_notMem — Mathlib

English

If the iUnion of subspaces equals the whole space, then one of the subspaces must be the whole space.

Русский

Если объединение подпространств даёт всю пространство, то одно из подпространств равно всему пространству.

LaTeX

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

Lean4

theorem biUnion_ne_univ_of_top_notMem (hs : ⊤ ∉ s) : ⋃ p ∈ s, (p : Set E) ≠ Set.univ :=
  by
  intro hcovers
  have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers
  have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex
  have : Nontrivial (E ⧸ p) := Submodule.Quotient.nontrivial_of_lt_top p (ne_of_mem_of_not_mem hp hs).lt_top
  have : Infinite (E ⧸ p) := Module.Free.infinite k (E ⧸ p)
  exact not_finite (E ⧸ p)

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