lt_eq_subset

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.lt_eq_subset

English

The strict less-than on Finset α coincides with the strict subset relation.

Русский

Строгое меньшее отношение на Finset α совпадает с отношением строгого включения.

LaTeX

$$$(\cdot < \cdot)\,(\text{Finset } α) = (\text{ }\subset \text{ } )$$$

Lean4

@[simp]
theorem lt_eq_subset : ((· < ·) : Finset α → Finset α → Prop) = (· ⊂ ·) :=
  rfl

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

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

Разделы

Аффилиация

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