English
Let X and Y be subsets with X ⊂ Y and the rank increase M.eRk X is strictly less than M.eRk Y. Then there exists an element y in Y not in X such that adding y to X raises the rank by exactly 1: M.eRk(X ∪ {y}) = M.eRk X + 1.
Русский
Пусть X ⊆ Y и M.eRk X < M.eRk Y. Тогда существует элемент y в Y \ X, такой что при добавлении y к X ранк возрастает на единицу: eRk(X ∪ {y}) = eRk(X) + 1.
LaTeX
$$$M.eRk X < M.eRk Y \\;\\Rightarrow\\; \\exists y \\in Y \\setminus X,\\; M.eRk(X \\cup \\{y\\}) = M.eRk X + 1$$$
Lean4
theorem exists_eRk_insert_eq_add_one_of_lt (h : M.eRk X < M.eRk Y) : ∃ y ∈ Y \ X, M.eRk (insert y X) = M.eRk X + 1 :=
by
have hz : ¬Y ∩ M.E ⊆ M.closure X := by
contrapose! h
simpa using M.eRk_mono h
obtain ⟨e, ⟨heZ, heE⟩, heX⟩ := not_subset.1 hz
refine ⟨e, ⟨heZ, fun heX' ↦ heX (mem_closure_of_mem' _ heX')⟩, eRk_insert_eq_add_one ⟨heE, heX⟩⟩
