toDFinsupp_lt_toDFinsupp

Mathlib.Data.DFinsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.toDFinsupp_lt_toDFinsupp

← MathLib Explorer

English

For s,t, toDFinsupp s < toDFinsupp t iff s < t.

Русский

Для s,t: toDFinsupp s < toDFinsupp t эквивалентно s < t.

LaTeX

$$$$ \\operatorname{toDFinsupp} s < \\operatorname{toDFinsupp} t \\iff s < t $$$$

Lean4

@[simp]
theorem toDFinsupp_lt_toDFinsupp : toDFinsupp s < toDFinsupp t ↔ s < t :=
  lt_iff_lt_of_le_iff_le' toDFinsupp_le_toDFinsupp toDFinsupp_le_toDFinsupp

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

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

Разделы

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

Аффилиация

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