Ico_subset_Ioo_pred_left

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Ico_subset_Ioo_pred_left

English

Icc a b ⊆ Ioc (pred a) b (simp lemma).

Русский

Icc a b ⊆ Ioc (pred a) b.

LaTeX

$$$$Icc(a,b) \subseteq Ioc(pred(a),b).$$$$

Lean4

@[simp]
theorem Ico_subset_Ioo_pred_left (a b : α) : Ico a b ⊆ Ioo (pred a) b :=
  Ico_subset_Ioo_pred_left_of_not_isMin <| not_isMin _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru