isRkFinite_inter_ground_iff — Mathlib

English

A set X is IsRkFinite iff its intersection with the ground set E is IsRkFinite: IsRkFinite(X ∩ E) ↔ IsRkFinite(X).

Русский

Множество X имеет конечный ранг эквивалентно тому, что X ∩ E имеет конечный ранг: IsRkFinite(X ∩ E) ↔ IsRkFinite(X).

LaTeX

$$$ M.IsRkFinite (X \\cap E) \\iff M.IsRkFinite X $$$

Lean4

@[simp]
theorem isRkFinite_inter_ground_iff : M.IsRkFinite (X ∩ M.E) ↔ M.IsRkFinite X :=
  let ⟨_I, hI⟩ := M.exists_isBasis' X
  ⟨fun h ↦ hI.isRkFinite_of_finite (hI.isBasis_inter_ground.finite_of_isRkFinite h), fun h ↦ h.subset inter_subset_left⟩

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