pure_le

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.pure_le

English

pure a ≤ s iff a ∈ s.

Русский

pure a ≤ s эквивалентно a ∈ s.

LaTeX

$$$\\mathrm{pure}(a) \\le s \\iff a \\in s$$$

Lean4

@[simp]
theorem pure_le {a : α} {s : Semiquot α} : pure a ≤ s ↔ a ∈ s :=
  Set.singleton_subset_iff

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

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

Разделы

Аффилиация

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