funext_iff_of_subsingleton — Mathlib

English

If α is a Subsingleton, then f x = g y is equivalent to f = g for any x,y in α.

Русский

Если α — подсинглотон, то f x = g y эквивалентно f = g для любых x,y ∈ α.

LaTeX

$$$$ f x = g y \\iff f = g. $$$$

Lean4

theorem funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) : f x = g y ↔ f = g :=
  by
  refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
  · rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
  · rw [h, Subsingleton.elim x y]

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