coe_mem

Mathlib.Data.SetLike.Basic

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

English

If x is an element of p, then its embedding in B is also a member of p.

Русский

Если x принадлежит p, то образ x в B принадлежит p.

LaTeX

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

Lean4

@[simp]
theorem coe_mem (x : p) : (x : B) ∈ p :=
  x.2

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

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

Разделы

Аффилиация

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