multipliable_bot

Mathlib.Topology.Algebra.InfiniteSum.Defs

URI: https://scilib.ai/kg/mathlib#multipliable_bot

English

If L is not NeBot, then for any f, f is Multipliable with respect to L.

Русский

Если L не является нижним пределом, то f — множимо по L.

LaTeX

$$$ \neg L.NeBot \rightarrow Multipliable f L $$$

Lean4

@[to_additive]
theorem multipliable_bot (hL : ¬L.NeBot) (f : β → α) : Multipliable f L :=
  ⟨1, hasProd_bot hL ..⟩

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

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

Разделы

Аффилиация

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