Theorems · Theorem · order theory

Set.Ioi_subset_Ici

∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ioi a ⊆ Set.Ici b

If a ≤ b, then (b, +∞) ⊆ [a, +∞). In preorders, this is just an implication. If you need the equivalence in dense linear orders, use Ioi_subset_Ici_iff.

Defined in

Mathlib.Order.Interval.Set.Basic

Cited by

5 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder