Ioo_eq_filter_ssubsets — Mathlib

English

Let s and t be finite subsets. The open-interval Ioo(s, t) corresponds exactly to the collection of u that are proper subsets of t and strictly contain s.

Русский

Пусть s и t — конечные подмножества. Открытый интервал Ioo(s, t) совпадает с множеством u, которые являются правильными подмножествами t и строго содержат s.

LaTeX

$$$Ioo(s,t) = \\{ u \\subseteq t \\mid s \\subsetneq u \\}$$$

Lean4

theorem Ioo_eq_filter_ssubsets : Ioo s t = {u ∈ t.ssubsets | s ⊂ u} := by ext; simp [and_comm]

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