pure_isPure

Mathlib.Data.Semiquot

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

English

IsPure (pure a).

Русский

IsPure (pure a).

LaTeX

$$$\mathrm{IsPure}(\mathrm{pure}(a))$$$

Lean4

@[simp]
theorem pure_isPure (a : α) : IsPure (pure a)
  | b, ab, c, ac => by
    rw [mem_pure] at ab ac
    rwa [← ac] at ab

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

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

Разделы

Аффилиация

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