preimage_comp — Mathlib

English

The preimage of s under the composition f.comp g equals g.preimage (f.preimage s).

Русский

Предобраз множества s по композиции f ∘ g равен предобразу по g от предобраза s по f.

LaTeX

$$$$ (f.comp g).preimage s = g.preimage (f.preimage s). $$$$

Lean4

@[simp]
theorem preimage_comp (f : β →. γ) (g : α →. β) (s : Set γ) : (f.comp g).preimage s = g.preimage (f.preimage s) :=
  by
  ext
  simp_rw [mem_preimage, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]
  rw [exists_comm]
  simp_rw [and_assoc, and_comm]

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