netMaxcard_eq_zero_iff — Mathlib

English

netMaxcard T F U n = 0 iff F = ∅.

Русский

netMaxcard T F U n = 0 тогда и только тогда, когда F = ∅.

LaTeX

$$netMaxcard(T,F,U,n)=0 \iff F=∅.$$

Lean4

theorem netMaxcard_eq_zero_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : netMaxcard T F U n = 0 ↔ F = ∅ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, netMaxcard_empty]⟩
  rw [eq_empty_iff_forall_notMem]
  intro x x_F
  have key := isDynNetIn_singleton T U n x_F
  rw [← Finset.coe_singleton] at key
  replace key := key.card_le_netMaxcard
  rw [Finset.card_singleton, Nat.cast_one, h] at key
  exact key.not_gt zero_lt_one

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