disjointed_bot — Mathlib

English

If there is a bottom element in the index order, disjointed at bottom equals f at bottom.

Русский

Если в порядке индексов есть минимальный элемент изображения bottom, то disjointed f bottom = f bottom.

LaTeX

$$$[OrderBot ι] (f)\Rightarrow disjointed f \mathrm{bot} = f \mathrm{bot}$$$

Lean4

@[simp]
theorem disjointed_bot [OrderBot ι] (f : ι → α) : disjointed f ⊥ = f ⊥ :=
  disjointed_of_isMin _ isMin_bot

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