prod_ne_top — Mathlib

English

A finite product of WithTop elements is not top if every factor is not top.

Русский

Пусть произведение конечного множества элементов WithTop не достигает верхнего элемента, если каждый фактор не равен верхнему.

LaTeX

$$$$ \left( \forall i \in s,\ f(i) \neq \top \right) \Rightarrow \prod_{i\in s} f(i) \neq \top. $$$$

Lean4

/-- A product of finite terms is finite. -/
theorem prod_ne_top (h : ∀ i ∈ s, f i ≠ ⊤) : ∏ i ∈ s, f i ≠ ⊤ :=
  prod_induction f (· ≠ ⊤) (fun _ _ ↦ mul_ne_top) coe_ne_top h

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