Iio_eq_ssubsets

Mathlib.Data.Finset.Interval

URI: https://scilib.ai/kg/mathlib#Finset.Iio_eq_ssubsets

English

The open lower interval Iio(s) equals the collection of all strict subsets of s.

Русский

Открытый нижний интервал Iio(s) совпадает с множеством строгих подмножеств s.

LaTeX

$$$Iio(s) = \\{ u \\subsetneq s \\}$$$

Lean4

theorem Iio_eq_ssubsets : Iio s = s.ssubsets := by ext; simp

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

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

Разделы

Аффилиация

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