mem_add — Mathlib

English

For fractional ideals I and J and any x in the ambient space, x ∈ I + J iff there exist i ∈ I and j ∈ J with i + j = x.

Русский

Для дробных идеалов I и J и любого x в расширяющем пространстве верно: x ∈ I + J тогда и только тогда, когда существуют i ∈ I, j ∈ J такие, что i + j = x.

LaTeX

$$$x \in I + J \iff \exists i \in I, \exists j \in J, i + j = x$$$

Lean4

theorem mem_add (I J : FractionalIdeal S P) (x : P) : x ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x := by
  rw [← mem_coe, coe_add, Submodule.add_eq_sup]; exact Submodule.mem_sup

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