equitableOn_empty

Mathlib.Data.Set.Equitable

URI: https://scilib.ai/kg/mathlib#Set.equitableOn_empty

English

The empty set is equitable with respect to any function f.

Русский

Пустаое множество устойчиво к любой функции f (равно справедливая).

LaTeX

$$$\text{EquitableOn}(\emptyset, f)$$$

Lean4

@[simp]
theorem equitableOn_empty [LE β] [Add β] [One β] (f : α → β) : EquitableOn ∅ f := fun a _ ha =>
  (Set.notMem_empty a ha).elim

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

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

Разделы

Аффилиация

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