surjective_of_right_cancellable_Prop

English

If h says that g1 ∘ f = g2 ∘ f implies g1 = g2 for all β → Prop-valued g, then f is surjective.

Русский

Если для любых g1,g2: β → Prop выполняется, что g1 ∘ f = g2 ∘ f ⇒ g1 = g2, то$f$ сюръективен.

LaTeX

$$$\left( \forall g_1,g_2:β \to \text{Prop},\ g_1 \circ f = g_2 \circ f \Rightarrow g_1 = g_2 \right) \Rightarrow \operatorname{Surjective}(f).$$$

Lean4

theorem surjective_of_right_cancellable_Prop (h : ∀ g₁ g₂ : β → Prop, g₁ ∘ f = g₂ ∘ f → g₁ = g₂) : Surjective f :=
  injective_comp_right_iff_surjective.mp h

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