mulDissociated_preimage — Mathlib

English

For a multiplicative equivalence e: β ≃* α, MulDissociated of the preimage e^{-1}'s of a set s is equivalent to MulDissociated(s).

Русский

Для мультивзаимной эквивалентности e: β ≃* α верно: MulDissociated (e^{-1}' s) эквивалентно MulDissociated s.

LaTeX

$$$$ \mathrm{MulDissociated}(e^{-1}' s) \iff \mathrm{MulDissociated}(s) \;\text{for } e:\beta \xrightarrow{\simeq}^* \alpha. $$$$

Lean4

@[to_additive (attr := simp)]
theorem mulDissociated_preimage (e : β ≃* α) : MulDissociated (e ⁻¹' s) ↔ MulDissociated s := by
  simp [MulDissociated, InjOn, ← e.finsetCongr.forall_congr_right, ← e.apply_eq_iff_eq, (Finset.map_injective _).eq_iff]

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