Ico_eq_filter_ssubsets

Mathlib.Data.Finset.Interval

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

English

The half-open interval Ico(s,t) equals the set of u in t.ssubsets with s ⊆ u.

Русский

Полуоткрытый интервал Ico(s,t) равен множеству u из t.ssubsets таких, что s ⊆ u.

LaTeX

$$$\\operatorname{Ico}(s,t) = \\{u \\in t.\\text{ssubsets} \\mid s \\subseteq u\\}.$$$

Lean4

theorem Ico_eq_filter_ssubsets : Ico s t = {u ∈ t.ssubsets | s ⊆ u} := by ext; simp [and_comm]

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

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

Разделы

Аффилиация

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