mem_coe

Mathlib.Data.SetLike.Basic

URI: https://scilib.ai/kg/mathlib#SetLike.mem_coe

English

For any x in B, x belongs to the coerced set p (as a Set B) exactly when x belongs to p.

Русский

Для любого x из B верно: x принадлежит преобразованному множеству p (как Set B) тогда и только тогда, когда x принадлежит p.

LaTeX

$$$ x \\in (p : Set B) \\iff x \\in p $$$

Lean4

@[simp]
theorem mem_coe {x : B} : x ∈ (p : Set B) ↔ x ∈ p :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru