English
If there is an absolute bound on the size of a subset satisfying P, then maximal subsets within a given X exist and can be characterized.
Русский
Если существует абсолютное ограничение на размер подмножества, удовлетворяющего P, то существуют максимальные подмножества внутри заданного X и их можно охарактеризовать.
LaTeX
$$$ \exists n\;\forall Y,\; P(Y) \Rightarrow Y.encode ≤ n$ implies ExistsMaximalSubsetProperty P X$$
Lean4
/-- If there is an absolute upper bound on the size of a set satisfying `P`, then the
maximal subset property always holds. -/
theorem _root_.Matroid.existsMaximalSubsetProperty_of_bdd {P : Set α → Prop} (hP : ∃ (n : ℕ), ∀ Y, P Y → Y.encard ≤ n)
(X : Set α) : ExistsMaximalSubsetProperty P X :=
by
obtain ⟨n, hP⟩ := hP
rintro I hI hIX
have hfin : Set.Finite (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) :=
by
rw [finite_iff_bddAbove, bddAbove_def]
simp_rw [ENat.le_coe_iff] at hP
use n
rintro x ⟨Y, ⟨hY, -, -⟩, rfl⟩
obtain ⟨n₀, heq, hle⟩ := hP Y hY
rwa [ncard_def, heq, ENat.toNat_coe]
obtain ⟨Y, ⟨hY, hIY, hYX⟩, hY'⟩ := Finite.exists_maximalFor' ncard _ hfin ⟨I, hI, rfl.subset, hIX⟩
refine ⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩
have hKfin : K.Finite := finite_of_encard_le_coe (hP K hPK)
refine (eq_of_subset_of_ncard_le hYK ?_ hKfin).symm.subset
exact hY' ⟨hPK, hIY.trans hYK, hKX⟩ (ncard_le_ncard hYK hKfin)
