English
netMaxcard T F U n = ⊤ iff for all k ∈ ℕ there exists s with IsDynNetIn and k ≤ |s|.
Русский
netMaxcard T F U n = ⊤ тогда и только тогда, когда для каждого k ∈ ℕ существует s с IsDynNetIn и k ≤ |s|.
LaTeX
$$netMaxcard(T,F,U,n)=\top \iff ∀ k ∈ ℕ, ∃ s : Finset X, IsDynNetIn(T,F,U,n,s) ∧ k ≤ s.card.$$
Lean4
theorem netMaxcard_infinite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
netMaxcard T F U n = ⊤ ↔ ∀ k : ℕ, ∃ s : Finset X, IsDynNetIn T F U n s ∧ k ≤ s.card :=
by
apply Iff.intro <;> intro h
· intro k
rw [netMaxcard, iSup_subtype', iSup_eq_top] at h
specialize h k (ENat.coe_lt_top k)
simp only [Nat.cast_lt, Subtype.exists, exists_prop] at h
obtain ⟨s, s_net, s_k⟩ := h
exact ⟨s, s_net, s_k.le⟩
· refine WithTop.eq_top_iff_forall_gt.2 fun k ↦ ?_
specialize h (k + 1)
obtain ⟨s, s_net, s_card⟩ := h
apply s_net.card_le_netMaxcard.trans_lt'
rw [ENat.some_eq_coe, Nat.cast_lt]
exact (lt_add_one k).trans_le s_card
