top_mem_of_biUnion_eq_univ — Mathlib

English

Given a finite index set, if the union of subspaces covers the whole space, some subspace must be the whole space.

Русский

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

LaTeX

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

Lean4

theorem top_mem_of_biUnion_eq_univ (hcovers : ⋃ p ∈ s, (p : Set E) = Set.univ) : ⊤ ∈ s :=
  by
  contrapose! hcovers
  exact Subspace.biUnion_ne_univ_of_top_notMem hcovers

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