isLoop_iff — Mathlib

English

If N ≤r M, then N.IsLoop e iff e ∈ N.E ∧ M.IsLoop e.

Русский

Если N является ограничением M, то N.IsLoop e эквивално e ∈ N.E и M.IsLoop e.

LaTeX

$$$ N.IsRestriction M \rightarrow (N.IsLoop e \iff (e \in N.E \land M.IsLoop e)) $$$

Lean4

theorem isLoop_iff (hNM : N ≤r M) : N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e :=
  by
  obtain ⟨R, hR, rfl⟩ := hNM
  simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]
  exact fun heR heE ↦ (heE (hR heR)).elim

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