mem_coe — Mathlib

English

A sphere, viewed as a subset, has the same elements as the corresponding sphere object; membership is preserved by the set-theoretic embedding.

Русский

Сфера, рассматриваемая как подмножество, содержит те же точки, что и соответствующий носитель сферы; членство сохраняется при вложении как множество.

LaTeX

$$$$ p \in (s : Set P) \iff p \in s. $$$$

Lean4

theorem mem_coe {p : P} {s : Sphere P} : p ∈ (s : Set P) ↔ p ∈ s :=
  Iff.rfl

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