extend_function_of_lt — Mathlib

English

If hs: #s < #α and h: α ≃ β, then there exists an extension g: α ≃ β of f on s.

Русский

Если hs: #s < #α и h: α ≃ β, тогда существует расширение g: α ≃ β на s.

LaTeX

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

Lean4

theorem extend_function_of_lt {α β : Type*} {s : Set α} (f : s ↪ β) (hs : #s < #α) (h : Nonempty (α ≃ β)) :
    ∃ g : α ≃ β, ∀ x : s, g x = f x := by
  cases fintypeOrInfinite α
  · exact extend_function_finite f h
  · apply extend_function f
    obtain ⟨g⟩ := id h
    haveI := Infinite.of_injective _ g.injective
    rw [← lift_mk_eq'] at h ⊢
    rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
    rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

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