mono

Mathlib.Data.Semiquot

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

English

IsPure is monotone with respect to ≤: if s ≤ t and IsPure t, then IsPure s.

Русский

IsPure монотонно по отношению к ≤: если s ≤ t и IsPure t, тогда IsPure s.

LaTeX

$$$(s \le t) \land \mathrm{IsPure}(t) \Rightarrow \mathrm{IsPure}(s)$$$

Lean4

theorem mono {s t : Semiquot α} (st : s ≤ t) (h : IsPure t) : IsPure s
  | _, as, _, bs => h _ (st as) _ (st bs)

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

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

Разделы

Аффилиация

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