mem_dpEqualizer_iff — Mathlib

English

An element x belongs to dpEqualizer hI hI' if and only if x ∈ I and hI.dpow n x = hI'.dpow n x for all n.

Русский

Элемент x принадлежит dpEqualizer hI hI', если и только если x ∈ I и для всех n выполняется hI.dpow n x = hI'.dpow n x.

LaTeX

$$$x \in dpEqualizer\ hI\ hI' \iff x \in I \wedge \forall n,\, hI.dpow n x = hI'.dpow n x$$

Lean4

theorem mem_dpEqualizer_iff {x : A} : x ∈ dpEqualizer hI hI' ↔ x ∈ I ∧ ∀ n : ℕ, hI.dpow n x = hI'.dpow n x := by
  simp [dpEqualizer, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_setOf_eq]

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