hasProd_of_isLUB — Mathlib

English

If IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) b, then HasProd f b.

Русский

Если IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) равно b, то HasProd f b.

LaTeX

$$IsLUB (Set.range fun s => ∏ i ∈ s, f i) b \\\\Rightarrow HasProd f b$$

Lean4

@[to_additive]
theorem hasProd_of_isLUB [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderTopology α]
    {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) b) : HasProd f b :=
  tendsto_atTop_isLUB (Finset.prod_mono_set' f) hf

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