eq_loopyOn_iff_loops — Mathlib

English

A matroid equals loopyOn E if and only if its loops are E and its ground is E.

Русский

Матроид равно loopyOn E тогда и только тогда, когда его петли равны E а множествоground равняется E.

LaTeX

$$$ M = \operatorname{loopyOn} E \iff M.loops = E \land M.E = E $$$

Lean4

theorem eq_loopyOn_iff_loops {E : Set α} : M = loopyOn E ↔ M.loops = E ∧ M.E = E
    where
  mp h := by rw [h, loops]; simp
  mpr
    | ⟨h, h'⟩ => by rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']

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