eq_loopyOn_iff_loops_eq — Mathlib

English

Same as eq_loopyOn_iff_loops: M equals loopyOn E iff M.loops = E and M.E = E.

Русский

То же самое, что и eq_loopyOn_iff_loops: M = loopyOn E тогда и только тогда, когда M.loops = E и M.E = E.

LaTeX

$$$ M = loopyOn E \iff M.loops = E \land M.E = E $$$

Lean4

theorem eq_loopyOn_iff_loops_eq {E : Set α} : M = loopyOn E ↔ M.loops = E ∧ M.E = E :=
  ⟨fun h ↦ by simp [h, loops], fun ⟨h, h'⟩ ↦ by rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']⟩

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