restrict_isLoop_iff — Mathlib

English

For any restricted matroid, (M restriction R).IsLoop e is equivalent to e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E).

Русский

Для ограниченного матроидa isLoop e эквивалентно e ∈ R и (M.IsLoop e или e ∉ M.E).

LaTeX

$$$ (M \restriction R).IsLoop e \iff e \in R \land (M.IsLoop e \lor e \notin M.E) $$$

Lean4

@[simp]
theorem restrict_isLoop_iff {R : Set α} : (M ↾ R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E) :=
  by
  simp only [isLoop_iff, restrict_closure_eq', empty_inter, mem_union, mem_inter_iff, mem_diff, ← closure_empty]
  tauto

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