coprodᵢ_eq_bot_iff

Mathlib.Order.Filter.Pi

URI: https://scilib.ai/kg/mathlib#Filter.coprodᵢ_eq_bot_iff

English

If all α i are nonempty, Coprodᵢ f = ⊥ iff f = ⊥.

Русский

Если все α i непусты, Coprodᵢ f = ⊥ тогда и только тогда, когда f = ⊥.

LaTeX

$$Coprodᵢ f = ⊥ ↔ f = ⊥$$

Lean4

@[simp]
theorem coprodᵢ_eq_bot_iff [∀ i, Nonempty (α i)] : Filter.coprodᵢ f = ⊥ ↔ f = ⊥ := by
  simpa [funext_iff] using coprodᵢ_neBot_iff.not

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

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

Разделы

Аффилиация

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