coe_sdiff — Mathlib

English

The coercion from Finset to Set commutes with SDiff: the set of s \\ t equals the set difference of the sets.

Русский

Переход из Finset в Set сохраняет операцию SDiff: множество разности равно разности множеств.

LaTeX

$$$ \\uparrow (s \\setminus t) = (s \\setminus t)^{\\text{Set}}. $$$

Lean4

@[simp, grind =, norm_cast]
theorem coe_sdiff (s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : Set α) :=
  Set.ext fun _ => mem_sdiff

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