preimage_div — Mathlib

English

If m is injective, then the preimage distributes over division: m⁻¹'(s/t) = m⁻¹'(s)/m⁻¹'(t) for s,t ⊆ β with appropriate range conditions.

Русский

Если m инъективен, то предобраз делитобразования взаимно распределяется: m⁻¹(s/t) = m⁻¹(s)/m⁻¹(t) при подходящих условиях.

LaTeX

$$m^{-1}(s/t) = m^{-1}(s)/m^{-1}(t)$$

Lean4

@[to_additive]
theorem preimage_div (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s / t) = m ⁻¹' s / m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

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