disjointed_add_one_sup

Mathlib.Algebra.Order.Disjointed

URI: https://scilib.ai/kg/mathlib#Monotone.disjointed_add_one_sup

← MathLib Explorer

English

If f is monotone, then disjointed f (i+1) ⊔ f i = f(i+1).

Русский

Если f монотонна, то disjointed f (i+1) ⊔ f i = f(i+1).

LaTeX

$$$ \text{Monotone}(f) \Rightarrow \forall i,\; \operatorname{disjointed} f (i+1) \; \sqcup\; f(i) = f(i+1) $$$

Lean4

protected theorem disjointed_add_one_sup {f : ι → α} (hf : Monotone f) (i : ι) :
    disjointed f (i + 1) ⊔ f i = f (i + 1) := by simpa only [succ_eq_add_one i] using hf.disjointed_succ_sup i

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

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

Разделы

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

Аффилиация

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