one_le_coverMincard_iff — Mathlib

English

The inequality 1 ≤ coverMincard T F U n holds exactly when F is nonempty.

Русский

Неравенство 1 ≤ coverMincard T F U n выполняется тогда, когда F непусто.

LaTeX

$$$1 \leq coverMincard(T,F,U,n) \iff F.Nonempty$$$

Lean4

theorem one_le_coverMincard_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    1 ≤ coverMincard T F U n ↔ F.Nonempty :=
  by
  rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]
  exact coverMincard_eq_zero_iff T F U n

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