loopyOn_isBasis_iff — Mathlib

English

For loopyOn E, IsBasis I X holds iff I = ∅ and X ⊆ E.

Русский

Для loopyOn(E) IsBasis I X верно тогда и только тогда, когда I = ∅ и X ⊆ E.

LaTeX

$$$ (loopyOn E).IsBasis I X \\iff I = ∅ \\land X \\subseteq E $$$

Lean4

@[simp]
theorem loopyOn_isBasis_iff : (loopyOn E).IsBasis I X ↔ I = ∅ ∧ X ⊆ E :=
  ⟨fun h ↦ ⟨loopyOn_indep_iff.mp h.indep, h.subset_ground⟩, by rintro ⟨rfl, hX⟩; rw [isBasis_iff]; simp⟩

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