mem_coe — Mathlib

English

The equivalence a ∈ (s : Set α) ↔ a ∈ s holds for all a and s, expressing that the membership in the underlying set matches membership in the quotient/subtype representation.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mem_coe (a : α) (s : Subtype (MeasurableSet : Set α → Prop)) : a ∈ (s : Set α) ↔ a ∈ s :=
  Iff.rfl

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