instUnion — Mathlib

English

There is a union operation on the subtype: the union of x and y is ⟨(x : Set α) ∪ y, x.prop.union y.prop⟩.

Русский

Существует операция объединения над подтипом: объединение x и y равно ⟨(x : Set α) ∪ y, x.prop.union y.prop⟩.

LaTeX

$$$$x \\cup y = \\langle (x : Set \\alpha) \\cup y, x.prop.union y.prop \\rangle.$$$$

Lean4

instance instUnion : Union (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun x y => ⟨(x : Set α) ∪ y, x.prop.union y.prop⟩⟩

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