mem_ofSet_iff

Mathlib.Data.PEquiv

URI: https://scilib.ai/kg/mathlib#PEquiv.mem_ofSet_iff

English

In terms of membership, a ∈ ofSet s b is equivalent to a = b ∧ a ∈ s.

Русский

Принадлежность a к ofSet s b эквивалентна a = b и a ∈ s.

LaTeX

$$$$ a \\in \\mathrm{ofSet}(s)\\, b \\iff a = b \\land a \\in s. $$$$

Lean4

theorem mem_ofSet_iff {s : Set α} [DecidablePred (· ∈ s)] {a b : α} : a ∈ ofSet s b ↔ a = b ∧ a ∈ s :=
  by
  dsimp [ofSet]
  grind

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

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

Разделы

Аффилиация

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