restrict_restrict_eq — Mathlib

English

Restricting to R2 inside a restriction to R1 equals restricting directly to R2, when R2 ⊆ R1.

Русский

Ограничение по R2 внутри ограничение по R1 равно ограничению по R2, если R2 ⊆ R1.

LaTeX

$$(M ↾ R1) ↾ R2 = M ↾ R2 \text{ whenever } R2 ⊆ R1$$

Lean4

theorem restrict_restrict_eq {R₁ R₂ : Set α} (M : Matroid α) (hR : R₂ ⊆ R₁) : (M ↾ R₁) ↾ R₂ = M ↾ R₂ :=
  by
  refine ext_indep rfl ?_
  simp only [restrict_ground_eq, restrict_indep_iff, and_congr_left_iff, and_iff_left_iff_imp]
  exact fun _ h _ _ ↦ h.trans hR

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