eq_of_ground_subset — Mathlib

English

If N ≤m M and M.E ⊆ N.E, then M and N are equal.

Русский

Если N ≤m M и E(M) ⊆ E(N), то M = N.

LaTeX

$$$ N \le_m M \land M.E \subseteq N.E \Rightarrow M = N $$$

Lean4

theorem eq_of_ground_subset (h : N ≤m M) (hE : M.E ⊆ N.E) : M = N :=
  by
  obtain ⟨C, D, rfl⟩ := h
  rw [delete_ground, contract_ground, subset_diff, subset_diff] at hE
  rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq, hE.2.symm.inter_eq,
    delete_empty]

Похожие утверждения