sigmaToPi_not_surjective_of_infinite

English

If the index set is infinite and all components are nontrivial, then sigmaToPi is not surjective.

Русский

Если множество индексов бесконечно и все компоненты ненулевые, то sigmaToPi не сюръективно.

LaTeX

$$$\\neg (\\operatorname{sigmaToPi} R).\\mathrm{Surjective}$$$

Lean4

theorem sigmaToPi_not_surjective_of_infinite : ¬(sigmaToPi R).Surjective := fun surj ↦
  have ⟨_, _, notMem⟩ := exists_maximal_notMem_range_sigmaToPi_of_infinite R
  (Set.range_eq_univ.mpr surj ▸ notMem) ⟨⟩

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