pred_wcovBy — Mathlib

English

For every a, pred(a) is a weak cover of a: pred(a) ≤ a and there is no element strictly between pred(a) and a.

Русский

Для каждого a, pred(a) является слабым покрытием a: pred(a) ≤ a и между ними нет элементов.

LaTeX

$$$ pred(a) \; \text{is a weak cover of } a:\ pred(a) \le a \land \n\forall x, pred(a) < x < a \Rightarrow \text{false} $$$

Lean4

theorem pred_wcovBy (a : α) : pred a ⩿ a :=
  ⟨pred_le a, fun _ hb nh => (le_pred_of_lt nh).not_gt hb⟩

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