pred_eq_csSup — Mathlib

English

In a ConditionallyCompleteLattice α with PredOrder α and NoMinOrder α, for all a, pred a equals sSup of Iio a.

Русский

В ConditionallyCompleteLattice α с PredOrder α и NoMinOrder α, для любого a: pred a = sSup (Iio a).

LaTeX

$$$ \\mathrm{pred}\\ a = \\mathrm{sSup}(\\mathrm{Iio}\\ a) $$$

Lean4

theorem pred_eq_csSup [ConditionallyCompleteLattice α] [PredOrder α] [NoMinOrder α] (a : α) :
    pred a = sSup (Set.Iio a) :=
  succ_eq_csInf (α := αᵒᵈ) a

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