of_leftInvOn — Mathlib

English

If f has a left inverse on A and g is a left-decomposed map, then g composed with f is decomposable on the image of A.

Русский

Если f имеет левый обратный на A, а g — слева разложимая отображение, то композиция g∘f раскладывается на образе A.

LaTeX

$$$\\mathrm{IsDecompOn}(f,A,S) \\wedge \\mathrm{LeftInvOn}(g,f,A) \\Rightarrow \\mathrm{IsDecompOn}(g, f[A], S^{-1}).$$$

Lean4

theorem of_leftInvOn {f g : X → X} {A : Set X} {S : Finset G} (hf : IsDecompOn f A S) (h : LeftInvOn g f A) :
    IsDecompOn g (f '' A) S⁻¹ := by
  rintro _ ⟨a, ha, rfl⟩
  rcases hf a ha with ⟨γ, γ_mem, hγ⟩
  use γ⁻¹, Finset.inv_mem_inv γ_mem
  rw [hγ, inv_smul_smul, ← hγ, h ha]

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