exists_eq_delete — Mathlib

English

Let N ≤_r M. Then there exists a subset D ⊆ E(M) such that N = M \\ D; i.e., every restriction arises by deleting some subset of the ground elements.

Русский

Пусть N ≤_r M. Тогда существует D ⊆ E(M), такое что N = M \\ D; то есть любое ограничение получается удалением некоторого подмножества базовых элементов.

LaTeX

$$$N\\le_r M \\Rightarrow \\exists D\\subseteq M.E,\\ N = M\\setminus D$$$

Lean4

theorem exists_eq_delete (hNM : N ≤r M) : ∃ D ⊆ M.E, N = M ＼ D :=
  ⟨M.E \ N.E, diff_subset, by obtain ⟨R, hR, rfl⟩ := hNM; rw [delete_compl, restrict_ground_eq]⟩

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