comp_right — Mathlib

English

If AntivaryOn f g s, then for any k, AntivaryOn (f ∘ k) (g ∘ k) (k⁻¹' s).

Русский

Если AntivaryOn f g s, то для любого k выполняется AntivaryOn (f ∘ k) (g ∘ k) (k⁻¹' s).

LaTeX

$$$\\operatorname{AntivaryOn}(f,g,s) \\Rightarrow \\forall k:\\\\iota' \\to \\\\iota, \\operatorname{AntivaryOn}(f \\circ k, g \\circ k, k^{-1}' s)$$$

Lean4

theorem comp_right (h : AntivaryOn f g s) (k : ι' → ι) : AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s) := fun _ hi _ hj =>
  h hi hj

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