coe_sdiff — Mathlib

English

The coercion of the upper-set sdiff t equals the set difference of the carrier of s and the lowerClosure of t.

Русский

Приведение множества верхнего типа s \nс точностью sdiff t совпадает с обычной операцией множеств: (с) \nразность множества s и нижнего замыкания t.

LaTeX

$$$ s.sdiff t = (s : Set\\,\\alpha) \\setminus \\operatorname{lowerClosure}(t) $$$

Lean4

@[simp, norm_cast]
theorem coe_sdiff (s : UpperSet α) (t : Set α) : s.sdiff t = (s : Set α) \ lowerClosure t :=
  rfl

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