comp_surjective — Mathlib

English

Reindexing a HasBasis by a surjective map preserves the HasBasis structure.

Русский

Перебиндирование базиса через сюръективное отображение сохраняет структуру базиса.

LaTeX

$$hasBasis l p s → (surjective g) → HasBasis (p ∘ g) (s ∘ g)$$

Lean4

theorem comp_surjective (h : l.HasBasis p s) {g : ι' → ι} (hg : Function.Surjective g) : l.HasBasis (p ∘ g) (s ∘ g) :=
  ⟨fun _ => h.mem_iff.trans hg.exists⟩

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