isRestriction_iff_exists

Mathlib.Combinatorics.Matroid.Minor.Restrict

URI: https://scilib.ai/kg/mathlib#Matroid.isRestriction_iff_exists

← MathLib Explorer

English

(N ≤r M) iff ∃ R ⊆ M.E with N = M|R.

Русский

(N ≤r M) эквивалентно существованию R ⊆ M.E такого, что N = M|R.

LaTeX

$$$ (N \\le_r M) \\iff \\exists R \\subseteq M.E, N = M|R $$$

Lean4

theorem isRestriction_iff_exists : (N ≤r M) ↔ ∃ R, R ⊆ M.E ∧ N = M ↾ R := by use IsRestriction.exists_eq_restrict;
  rintro ⟨R, hR, rfl⟩; exact restrict_isRestriction M R hR

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru