mem_mk_set

Mathlib.Data.SetLike.Basic

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

English

For X, a Set p of X, a set U, and h: p U, an element x belongs to Subtype.mk U h if and only if x ∈ U.

Русский

Пусть X, U ⊆ X и h: U, тогда x ∈ Subtype.mk U h тогда и только тогда, когда x ∈ U.

LaTeX

$$$ x \in Subtype.mk U h \ \text{iff} \ x \in U $$$

Lean4

@[simp]
theorem mem_mk_set {X} {p : Set X → Prop} {U : Set X} {h : p U} {x : X} : x ∈ Subtype.mk U h ↔ x ∈ U :=
  Iff.rfl

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

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

Разделы

Аффилиация

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