Ici_add_one_eq_Ioi — Mathlib

English

For every a, the set of elements at least a+1 equals the set of elements strictly greater than a; i.e. Ici(a+1) = Ioi(a).

Русский

Для каждого a множество элементов, не меньших чем a+1, равно множеству элементов строго больших чем a; то есть Ici(a+1) = Ioi(a).

LaTeX

$$$\text{Ici}(a+1) = \text{Ioi}(a)$$$

Lean4

theorem Ici_add_one_eq_Ioi (a : α) : Ici (a + 1) = Ioi a := by simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

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