instSDiff — Mathlib

English

There is a set difference operation on the subtype: x \\ y = ⟨x \\ y, x.prop.diff y.prop⟩.

Русский

Существует операция симметричной разности на подтипе: x \\ y = ⟨x \\ y, x.prop.diff y.prop⟩.

LaTeX

$$$$x \\setminus y = ⟨x \\setminus y, x.prop.diff y.prop\\rangle.$$$$

Lean4

instance instSDiff : SDiff (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun x y => ⟨x \ y, x.prop.diff y.prop⟩⟩
    -- TODO: Why does it complain that `x ⇨ y` is noncomputable?

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