coe_sdiff — Mathlib

English

The underlying set of the set difference equals the difference of underlying sets.

Русский

Основанное множество разности равно разности множеств.

LaTeX

$$$$ ((s \\ t : L.DefinableSet A α) : Set(α \\to M)) = (s : Set(α \\to M)) \\ (t : Set(α \\to M)). $$$$

Lean4

@[simp, norm_cast]
theorem coe_sdiff (s t : L.DefinableSet A α) :
    ((s \ t : L.DefinableSet A α) : Set (α → M)) = (s : Set (α → M)) \ (t : Set (α → M)) :=
  rfl

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