min

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.IsPure.min

← MathLib Explorer

English

If t is pure, then s ≤ t iff s = t.

Русский

Если t чистый, то s ≤ t эквивалентно s = t.

LaTeX

$$$\mathrm{IsPure}(t) \rightarrow (s \le t \iff s = t)$$$

Lean4

theorem min {s t : Semiquot α} (h : IsPure t) : s ≤ t ↔ s = t :=
  ⟨fun st => le_antisymm st <| by rw [eq_pure h, eq_pure (h.mono st)]; simpa using h _ (get_mem _) _ (st <| get_mem _),
    le_of_eq⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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