equitableOn — Mathlib

English

If S is a subsingleton (has at most one element), then S is equitable on f for any f.

Русский

Если S состоит из не более чем одного элемента, то S является EquitableOn по отношению к любой функции f.

LaTeX

$$$$ \\text{If } S \\text{ is Subsingleton, then } S.\\mathrm{EquitableOn}(f). $$$$

Lean4

theorem equitableOn {s : Set α} (hs : s.Subsingleton) (f : α → β) : s.EquitableOn f := fun i j hi hj =>
  by
  rw [hs hi hj]
  exact le_add_of_nonneg_right zero_le_one

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