mk

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.Mem.mk

English

For any α, A: α → PSet, and a ∈ α, the pair (a, identity) witnesses a membership A(a) ∈ mk α A.

Русский

Для любого α, A: α → PSet, и a ∈ α существует доказательство A(a) ∈ mk α A.

LaTeX

$$$\\\\forall {\\\\alpha : Type u} (A : \\\\alpha \\\\rightarrow PSet) (a : \\\\alpha), A a \\\\in mk \\\\alpha A$$$

Lean4

theorem mk {α : Type u} (A : α → PSet) (a : α) : A a ∈ mk α A :=
  ⟨a, Equiv.refl (A a)⟩

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

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

Разделы

Аффилиация

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