instInsert — Mathlib

English

Given a ∈ α and s ∈ Subtype(MeasurableSet), there is an insertion operation producing a new measurable-subtype whose underlying set is Insert.insert a (s : Set α) and whose measurability follows from s.prop.insert a.

Русский

Пусть a ∈ α и s ∈ Subtype(MeasurableSet). Существет операция вставки, которая порождает новый подтип измеримых множеств с подмножством Insert.insert a (s : Set α) и свойством измеримости s.prop.insert a.

LaTeX

$$$$\\text{Insert.insert } a\\ s \\quad\\text{has underlying set } \\text{Insert.insert } a (s : Set α) \\text{ and property } s.prop.insert a.$$$$

Lean4

instance instInsert [MeasurableSingletonClass α] : Insert α (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun a s => ⟨insert a (s : Set α), s.prop.insert a⟩⟩

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