mapsTo_iff_exists_map_subtype — Mathlib

English

Let f: A→B and S⊆A, T⊆B. Then f maps S into T if and only if there exists a function g: S→T such that for every x ∈ S, f(x) = g(x).

Русский

Пусть f: A→B и S⊆A, T⊆B. Тогда f отображает S в T тогда и только тогда, когда существует функция g: S→T такая, что для любого x ∈ S выполняется f(x) = g(x).

LaTeX

$$$(\text{MapsTo } f\ s\ t) \iff \exists g: s \to t, \forall x: s, f\ x = g\ x$$$

Lean4

theorem mapsTo_iff_exists_map_subtype : MapsTo f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x :=
  ⟨fun h => ⟨h.restrict f s t, fun _ => rfl⟩, fun ⟨g, hg⟩ x hx =>
    by
    rw [hg ⟨x, hx⟩]
    apply Subtype.coe_prop⟩

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