elem_mem

Mathlib.Data.Set.CoeSort

URI: https://scilib.ai/kg/mathlib#Set.elem_mem

Lean4

@[simp]
theorem elem_mem {σ α} [I : Membership σ α] {S} : @Set.Elem σ (@Membership.mem σ α I S) = { x // x ∈ S } :=
  rfl

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

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

Разделы

Аффилиация

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