instMembership — Mathlib

English

For every a in α and every s in the measurable-set subtype, the membership of a in the underlying set coincides with membership in the subtype element: a ∈ (s : Set α) iff a ∈ s.

Русский

Для каждого элемента a в α и каждого элемента s из подтипа измеримых множеств верно, что a принадлежит подмножеству (s : Set α) тогда и только тогда, когда a принадлежит самому s.

LaTeX

$$$$a \\in (s : Set \\alpha) \\iff a \\in s.$$$$

Lean4

instance instMembership : Membership α (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun s a => a ∈ (s : Set α)⟩

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