eq_of_subset_indep

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.eq_of_subset_indep

English

If I is a basis of X and J is independent with I ⊆ J ⊆ X, then I = J.

Русский

Если I — база X, а J независим и I ⊆ J ⊆ X, то I = J.

LaTeX

$$$ M.IsBasis I X \land M.Indep J \land I \subseteq J \land J \subseteq X \Rightarrow I = J $$$

Lean4

theorem eq_of_subset_indep (hI : M.IsBasis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) : I = J :=
  hIJ.antisymm (hI.1.2 ⟨hJ, hJX⟩ hIJ)

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

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

Разделы

Аффилиация

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