iff_exists — Mathlib

English

Equivalent formulation: IsHomogeneous is characterized by the existence of a generating set of homogeneous elements.

Русский

Эквивалентная формулировка: гомогенность задаётся существованием порождающего множества однородных элементов.

LaTeX

$$I.IsHomogeneous 𝒜 I ⇔ ∃ S : Set (homogeneousSubmonoid 𝒜), I = Ideal.span (image Subtype.val S)$$

Lean4

theorem iff_exists : I.IsHomogeneous 𝒜 ↔ ∃ S : Set (homogeneousSubmonoid 𝒜), I = Ideal.span ((↑) '' S) :=
  by
  rw [Ideal.IsHomogeneous.iff_eq, eq_comm]
  exact ((Set.image_preimage.compose (Submodule.gi _ _).gc).exists_eq_l _).symm

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