mem_valueMonoid_iff — Mathlib

English

For units b in B, membership b ∈ valueMonoid f is equivalent to b ∈ preimage of range f under the coefficient map.

Русский

Для единиц b в B эквивалентно: b ∈ valueMonoid f тогда и только тогда, когда b ∈ предобразу множества значений range f по соответствующему отображению.

LaTeX

$$b ∈ valueMonoid f ↔ b ∈ (↑)^{-1}'(range f)$$

Lean4

theorem mem_valueMonoid_iff {b : Bˣ} : b ∈ valueMonoid f ↔ b ∈ (↑) ⁻¹' (range f) :=
  Iff.rfl

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