English
netMaxcard T F U n < ∞ iff there exists a finite s with IsDynNetIn T F U n s and (s.card) = netMaxcard T F U n.
Русский
netMaxcard T F U n < ∞ тогда и только тогда, когда существует конечное s с IsDynNetIn T F U n s и card(s) = netMaxcard T F U n.
LaTeX
$$netMaxcard(T,F,U,n) < \top \iff ∃ s : Finset X, IsDynNetIn(T,F,U,n,s) ∧ (s.card : ℕ∞) = netMaxcard(T,F,U,n).$$
Lean4
theorem netMaxcard_finite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
netMaxcard T F U n < ⊤ ↔ ∃ s : Finset X, IsDynNetIn T F U n s ∧ (s.card : ℕ∞) = netMaxcard T F U n :=
by
apply Iff.intro <;> intro h
· obtain ⟨k, k_max⟩ := WithTop.ne_top_iff_exists.1 h.ne
rw [← k_max]
simp only [ENat.some_eq_coe, Nat.cast_inj]
-- The criterion we want to use is `Nat.sSup_mem`. We rewrite `netMaxcard` with an `sSup`,
-- then check its `BddAbove` and `Nonempty` hypotheses.
have : netMaxcard T F U n = sSup (WithTop.some '' (Finset.card '' {s : Finset X | IsDynNetIn T F U n s})) :=
by
rw [netMaxcard, ← image_comp, sSup_image]
simp only [mem_setOf_eq, ENat.some_eq_coe, Function.comp_apply]
rw [this] at k_max
have h_bdda : BddAbove (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) :=
by
refine ⟨k, mem_upperBounds.2 ?_⟩
simp only [mem_image, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro s h
rw [← WithTop.coe_le_coe, k_max]
apply le_sSup
simp only [ENat.some_eq_coe, mem_image, mem_setOf_eq, Nat.cast_inj, exists_eq_right]
exact Filter.frequently_principal.mp fun a ↦ a h rfl
have h_nemp : (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}).Nonempty :=
by
refine ⟨0, ?_⟩
simp only [mem_image, mem_setOf_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
exact isDynNetIn_empty
rw [← WithTop.coe_sSup' h_bdda, ENat.some_eq_coe, Nat.cast_inj] at k_max
have key := Nat.sSup_mem h_nemp h_bdda
rw [← k_max, mem_image] at key
simp only [mem_setOf_eq] at key
exact key
· obtain ⟨s, _, s_card⟩ := h
rw [← s_card]
exact WithTop.coe_lt_top s.card
