pairwise_disjoint_on_Ico_pred — Mathlib

English

In any order with LT, not being IsSuccPrelimit at a is equivalent to the existence of a witness b with CovBy b a.

Русский

В любом порядке с LT невозможность IsSuccPrelimit в точке a эквивалентна существованию b, такого что CovBy b a.

LaTeX

$$$\lnot IsSuccPrelimit(a) \iff \exists b\, CovBy(b,a)$$$

Lean4

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ico (f n) (f (Order.pred n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_pred [PredOrder α] [Preorder β] {f : α → β} (hf : Antitone f) :
    Pairwise (Disjoint on fun n => Ico (f n) (f (pred n))) :=
  hf.dual_left.pairwise_disjoint_on_Ico_succ

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