dom_comp — Mathlib

English

The domain of the composition f.comp g equals the preimage under g of the domain of f: (f.comp g).Dom = g.preimage f.Dom.

Русский

Область определения композиции f ∘ g равна предобразу области определения f по g: (f.comp g).Dom = g.preimage f.Dom.

LaTeX

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

Lean4

@[simp]
theorem dom_comp (f : β →. γ) (g : α →. β) : (f.comp g).Dom = g.preimage f.Dom :=
  by
  ext
  simp_rw [mem_preimage, mem_dom, comp_apply, Part.mem_bind_iff, ← exists_and_right]
  rw [exists_comm]
  simp_rw [and_comm]

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