ext' — Mathlib

English

Two homogeneous submodules are equal if and only if their toSubmodule maps are equal.

Русский

Два однородных подмодуля равны тогда и только тогда, когда их отображения toSubmodule равны.

LaTeX

$$$$ I.toSubmodule = J.toSubmodule \iff I = J. $$$$

Lean4

/-- The set-theoretic extensionality of `HomogeneousSubmodule`.
-/
theorem ext' {I J : HomogeneousSubmodule 𝒜 ℳ} (h : ∀ i, ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J) : I = J :=
  by
  ext
  rw [I.isHomogeneous.mem_iff, J.isHomogeneous.mem_iff]
  apply forall_congr'
  exact fun i ↦ h i _ (decompose ℳ _ i).2

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