pi_eq_bot_iff — Mathlib

English

The pi-product over univ is bottom if and only if every S_i is bottom.

Русский

Произведение π по единичному множеству равно нулю тогда и только тогда, когда каждый S_i равен нулю.

LaTeX

$$$ pi Set.univ S = \bot \iff \forall i, S i = \bot $$$

Lean4

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

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