singleton_mem_jointlySurjectivePrecoverage_iff

English

In Types, Presieve.singleton f belongs to jointlySurjectivePrecoverage Y if and only if f is surjective.

Русский

В типах, Presieve.singleton f принадлежит jointlySurjectivePrecoverage Y тогда, когда f сюръективна.

LaTeX

$$$Presieve.singleton f \in jointlySurjectivePrecoverage Y \iff Function.Surjective f$$$

Lean4

theorem singleton_mem_jointlySurjectivePrecoverage_iff {X Y : Type u} {f : X ⟶ Y} :
    Presieve.singleton f ∈ jointlySurjectivePrecoverage Y ↔ Function.Surjective f :=
  by
  rw [mem_jointlySurjectivePrecoverage_iff]
  refine ⟨fun hf x ↦ ?_, fun hf x ↦ ⟨X, f, ⟨⟩, by simp [hf.range_eq]⟩⟩
  obtain ⟨_, _, ⟨⟩, hx⟩ := hf x
  exact hx

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