image_comp_equiv — Mathlib

English

Definability is preserved under applying an equivalence to the index set and taking image.

Русский

Определяемость сохраняется после применения эквивалентности к индексу и взятия образа.

LaTeX

$$$A.Definable L s \rightarrow \forall (f : Equiv \alpha \beta), A.Definable L (Set.image (fun g => g \circ (EquivLike.toFunLike.coe f)) s).$$$

Lean4

theorem image_comp_equiv {s : Set (β → M)} (h : A.Definable L s) (f : α ≃ β) :
    A.Definable L ((fun g : β → M => g ∘ f) '' s) :=
  by
  refine (congr rfl ?_).mp (h.preimage_comp f.symm)
  rw [image_eq_preimage_of_inverse]
  · intro i
    ext b
    simp only [Function.comp_apply, Equiv.apply_symm_apply]
  · intro i
    ext a
    simp

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