infinite_of_infinite

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.infinite_of_infinite

← MathLib Explorer

English

If B is a base of M and B is infinite, then RankInfinite M.

Русский

Если B — база M и B бесконечна, то RankInfinite M.

LaTeX

$$$(hB : M.IsBase B) \to B.Infinite \to RankInfinite M$$$

Lean4

theorem infinite_of_infinite (hB : M.IsBase B) (h : B.Infinite) (hB₁ : M.IsBase B₁) : B₁.Infinite :=
  by_contra (fun hB_inf ↦ (hB₁.finite_of_finite (not_infinite.mp hB_inf) hB).not_infinite h)

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

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

Разделы

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

Аффилиация

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