Ioc_eq_filter_powerset — Mathlib

English

Let s and t be finite subsets of a set; then the interval Ioc(s, t) consists exactly of those finite subsets u that are contained in t and strictly contain s.

Русский

Пусть s и t — конечные подмножества множества. Тогда интервал Ioc(s, t) состоит ровно из таких подмножеств u, которые содержатся в t и строго содержат s.

LaTeX

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

Lean4

theorem Ioc_eq_filter_powerset : Ioc s t = {u ∈ t.powerset | s ⊂ u} := by ext; simp [and_comm]

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