Icc_eq_filter_powerset

Mathlib.Data.Finset.Interval

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

English

The closed interval Icc(s,t) can be described as the set of all u in t.powerset such that s ⊆ u.

Русский

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

LaTeX

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

Lean4

theorem Icc_eq_filter_powerset : Icc s t = {u ∈ t.powerset | s ⊆ u} := by ext; simp [and_comm]

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

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

Разделы

Аффилиация

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