coe_erase — Mathlib

English

The erase of s at a equals the underlying set difference: (s.erase a) = (s : Set α) \\ lowerClosure({a}).

Русский

Удаление a из s в виде множества эквивалентно разности: (s.erase a) = (s как множество) \\ нижнее замыкание {a}.

LaTeX

$$$ s.erase a = (s : Set α) \\ \\operatorname{lowerClosure}(\\{a\\}) $$$

Lean4

@[simp, norm_cast]
theorem coe_erase (s : UpperSet α) (a : α) : s.erase a = (s : Set α) \ LowerSet.Iic a :=
  rfl

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