coe_sdiff — Mathlib

English

The underlying set of the clopen difference s \ t equals the set difference of the underlying sets: ↑(s \ t) = s \ t.

Русский

Подмножество клопного множества разности определяется как множество разностей: ↑(s \ t) = s \ t.

LaTeX

$$$\uparrow (s \ t) = (s \ t) \,\text{as a set} \\ (s,t \in \mathrm{Clopens}(\alpha)).$$$

Lean4

@[simp, norm_cast]
theorem coe_sdiff (s t : Clopens α) : ↑(s \ t) = (s \ t : Set α) :=
  rfl

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