Remove Subtype.coind_surjective?

Stream: mathlib4

[Vasilii Nesterov]

Conditions of docs#Subtype.coind_surjective and docs#Subtype.coind_bijective

theorem coind_surjective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Surjective f) :
    Surjective (coind f h)

theorem coind_bijective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Bijective f) :
    Bijective (coind f h)

imply that p is always true, so the subtype is trivial and the theorems are quite useless. Should we remove them?

[Notification Bot]

This topic was moved here from #mathlib4 > Subtype.coind_surjective by Vasilii Nesterov.

[Jireh Loreaux]

I think that, although they are mathematically trivial, they may still have utility. The issue is that you may have a function for which you restrict the codomain to a subtype. For example, you restrict the codomain to a submodule. Then in a certain instance, that submodule happens to be ⊤. So your subtype is equivalent to the full type, but it's technically still a subtype.

[Vasilii Nesterov]

I don't think I understand. In any situation where one can prove ∀ a, p (f a) and Surjective f, one can also prove ∀ b, p b (which seems easier), and then use, for example, docs#Equiv.subtypeUnivEquiv. We can also add the following as a lemma:

example (α β : Type) (f : α → β) (p : β → Prop) (h : ∀ a, p (f a)) (hf : Function.Surjective f) :
    ∀ b, p b := fun b ↦ (hf b).choose_spec ▸ h _

[Aaron Liu]

can we maybe change them to only require surjectivity/bijectivity onto the subtype (like docs#Set.SurjOn and docs#Set.BijOn)

[Jireh Loreaux]

Sure, I completely agree, I'm just arguing that there's no reason to remove these lemmas so that the user doesn't have to go through the effort of fiding and using docs#Equiv.subtypeUnivEquiv. Especially if we use fun_prop (I'm not sure if this PR for adding Surjective and friends to the fun_prop hierarchy every went through), it will need to have things mentioning Subtype.coind.

[Vasilii Nesterov]

I agree. In #26149 I proved

theorem Subtype.coind_surjective' {α β} {f : α → β} {p : Set β} (h : ∀ a, f a ∈ p)
    (hf : Set.SurjOn f Set.univ p) :
    (Subtype.coind f h).Surjective

[Jireh Loreaux]

But Aaron's suggestion is even more relevant (than what I said above).

[Vasilii Nesterov]

I propose to replace coind_surjective and coind_bijective with SurjOn and BijOn versions. Should I PR it?