English
The ENatural value of spanRank equals the infimum over all sets with span equal to p of their encard.
Русский
Значение spanRank в ENat равно infimum по всем множествам s, удовлетворяющим span R s = p, их encard.
LaTeX
$$$p.spanRank.toENat = \inf_{s:\, span R s = p} s.encard$$$
Lean4
theorem spanRank_toENat_eq_iInf_encard (p : Submodule R M) :
p.spanRank.toENat = (⨅ (s : Set M) (_ : span R s = p), s.encard) :=
by
rw [spanRank]
apply le_antisymm
· refine le_iInf₂ (fun s hs ↦ ?_)
rw [Set.encard, ENat.card]
exact toENat.monotone' (ciInf_le' _ (⟨s, hs⟩ : { s : Set M // span R s = p }))
· have := congrFun toENat_comp_ofENat.{u}.symm (⨅ (s : Set M) (_ : span R s = p), s.encard)
rw [id_eq] at this; rw [this]
refine toENat.monotone' (le_ciInf fun s ↦ ?_)
have : ofENat.{u} (⨅ (s' : Set M), ⨅ (_ : span R s' = p), s'.encard) ≤ ofENat s.1.encard :=
ofENatHom.monotone' (le_trans (ciInf_le' _ s.1) (ciInf_le' _ s.2))
apply le_trans this
rw [Set.encard, ENat.card]
exact Cardinal.ofENat_toENat_le _
