coind_surjective — Mathlib

English

If h ensures p after applying f and f is surjective, then coind f h is surjective.

Русский

Если h обеспечивает свойство p после применения f и f сюръективен, то coind f h сюръективно.

LaTeX

$$$\\text{Surjective}(\\mathrm{Subtype}.coind f h)$$$

Lean4

theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Surjective f) :
    Surjective (coind f h) := fun x ↦
  let ⟨a, ha⟩ := hf x
  ⟨a, coe_injective ha⟩

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