pi_bot — Mathlib

English

The pi-product over the universal index set of bottom submonoids is bottom; i.e., the product of bottoms is bottom.

Русский

Произведение π по всеобщему множеству индексов из нижних подмoноидов равно нижнему.

LaTeX

$$$ (\pi Set.univ (fun i => (⊥ : Submonoid (M i)))) = \bot $$$

Lean4

@[to_additive]
theorem pi_bot : (pi Set.univ fun i => (⊥ : Submonoid (M i))) = ⊥ :=
  ext fun x => by simp [mem_pi, funext_iff]

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