bot_pow

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.bot_pow

← MathLib Explorer

English

(⊥ : Filter α)^n = ⊥ for all n ≠ 0.

Русский

(⊥)^n = ⊥ для любого n ≠ 0.

LaTeX

$$$\forall n \in \mathbb{N},\ n \neq 0 \Rightarrow (\bot : \mathrm{Filter}(\alpha))^n = \bot.$$$

Lean4

@[to_additive (attr := simp) nsmul_bot]
theorem bot_pow {n : ℕ} (hn : n ≠ 0) : (⊥ : Filter α) ^ n = ⊥ := by rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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