isBasis_iff_empty_of_subset_loops

English

If X ⊆ M.loops, then M.IsBasis I X iff I = ∅.

Русский

Если X ⊆ M.loops, то I является базисом X тогда и только тогда, когда I = ∅.

LaTeX

$$$ X \subseteq M.loops \Rightarrow M.IsBasis I X \iff I=\emptyset $$$

Lean4

theorem isBasis_iff_empty_of_subset_loops (hX : X ⊆ M.loops) : M.IsBasis I X ↔ I = ∅ :=
  by
  refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
  have := (closure_eq_loops_of_subset hX) ▸ h.isBasis_closure_right
  simpa using this

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