coverMincard_eq_zero_iff — Mathlib

English

The value coverMincard T F U n is zero if and only if F is empty.

Русский

Значение coverMincard T F U n равно нулю тогда, когда F пусто.

LaTeX

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

Lean4

theorem coverMincard_eq_zero_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : coverMincard T F U n = 0 ↔ F = ∅ :=
  by
  refine ⟨fun h ↦ subset_empty_iff.1 ?_, fun F_empt ↦ by rw [F_empt, coverMincard_empty]⟩
  have := coverMincard_finite_iff T F U n
  rw [h, eq_true ENat.top_pos, true_iff] at this
  simp only [IsDynCoverOf, Finset.mem_coe, Nat.cast_eq_zero, Finset.card_eq_zero, exists_eq_right, Finset.notMem_empty,
    iUnion_of_empty, iUnion_empty] at this
  exact this

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