mem_mk — Mathlib

English

For the Sublocale mk carrier sInf_mem' himp_mem' membership description, a is in the Sublocale iff a is in the carrier.

Русский

Для индикатора Sublocale mk cоответствующая принадлежность соответствует принадлежности в базовом множестве.

LaTeX

$$$a \in mk\,carrier\,sInf\_mem'\,himp\_mem' \leftrightarrow a \in carrier$$$

Lean4

@[simp]
theorem mem_mk (carrier : Set X) (sInf_mem' himp_mem') : a ∈ mk carrier sInf_mem' himp_mem' ↔ a ∈ carrier :=
  .rfl

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