coverMincard_empty — Mathlib

English

If F is empty, then for any T and U and any n, the minimal cover cardinal is zero: coverMincard T ∅ U n = 0.

Русский

Если F пусто, то минимальная карта покрытия равна нулю: coverMincard T ∅ U n = 0.

LaTeX

$$$coverMincard(T,\emptyset,U,n) = 0$$$

Lean4

@[simp]
theorem coverMincard_empty {T : X → X} {U : Set (X × X)} {n : ℕ} : coverMincard T ∅ U n = 0 :=
  (sInf_le (by simp [IsDynCoverOf])).antisymm (zero_le (coverMincard T ∅ U n))

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