range_comp — Mathlib

English

Applying h and then h.symm to a set returns the set and preserves set-theoretic relations.

Русский

Применение h, затем h.symm к множеству возвращает само множество и сохраняет отношения множеств.

LaTeX

$$$h[ S ] \xrightarrow{h.symm} S$; i.e., $h.symm[h[S]] = S$.$$

Lean4

@[simp, mfld_simps]
nonrec theorem range_comp {α} (h : M ≃ₘ^n⟮I, J⟯ N) (f : α → M) : range (h ∘ f) = h.symm ⁻¹' range f := by
  rw [range_comp, image_eq_preimage]

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