isPure_iff

Mathlib.Data.Semiquot

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

English

IsPure s if and only if there exists a with s = pure a.

Русский

IsPure s тогда и только тогда, когда существует a такое, что s = pure a.

LaTeX

$$$\mathrm{IsPure}(s) \iff \exists a, \ s = \mathrm{pure}(a)$$$

Lean4

theorem isPure_iff {s : Semiquot α} : IsPure s ↔ ∃ a, s = pure a :=
  ⟨fun h => ⟨_, eq_pure h⟩, fun ⟨_, e⟩ => e.symm ▸ pure_isPure _⟩

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

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

Разделы

Аффилиация

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