extend_function_finite — Mathlib

English

If α is finite and f: s → β is an embedding with a witness that α ≃ β, then there exists g: α ≃ β extending f on s.

Русский

Если α конечен и есть вложение f: s → β с существованием биекции α ≃ β, то существует биекция g: α ≃ β, которая расширяет f на s.

LaTeX

$$$\\exists g: \\alpha \\cong \\beta, \\forall x:\\, s, g(x) = f(x)$$$

Lean4

theorem extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : s ↪ β) (h : Nonempty (α ≃ β)) :
    ∃ g : α ≃ β, ∀ x : s, g x = f x := by
  apply extend_function.{u, v} f
  obtain ⟨g⟩ := id h
  rw [← lift_mk_eq.{u, v, max u v}] at h
  rw [← lift_mk_eq.{u, v, max u v}, mk_compl_eq_mk_compl_finite_lift.{u, v, max u v} h]
  rw [mk_range_eq_lift.{u, v, max u v}]; exact f.2

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