pi_eq_bot_iff

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#Subgroup.pi_eq_bot_iff

← MathLib Explorer

English

For a family H, pi Set.univ H = ⊥ iff every H i = ⊥.

Русский

Для семейства H, pi Set.univ H = ⊥ тогда и только если каждый H i = ⊥.

LaTeX

$$$ \mathrm{pi} \mathrm{Set.univ} H = \bot \iff \forall i, H i = \bot $$$

Lean4

@[to_additive]
theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ i, H i = ⊥ :=
  by
  simp_rw [SetLike.ext'_iff]
  exact Set.univ_pi_eq_singleton_iff

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru