[Merged by Bors] - feat(data/*set): some finite sets lemmas

[PatrickMassot]

Co-authored-by: Bhavik Mehta, Kevin Buzzard, Anne Baanen, Eric Rodriguez

---

See Zulip at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/maximal.20independent.20family and
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finite.20stuff

[eric-wieser]

This name is a little similar to equiv.to_embedding.

Also, perhaps we should generalize ↥s to subtype p.

[eric-wieser]

That is,

/-- Given an equivalence to a subtype, produce an embedding to the elements of enclosing type. -/
@[simps]
def equiv.embedding_of_subtype {α β : Type*} {p : β → Prop} (e : α ≃ subtype p) : α ↪ β :=
e.to_embedding.trans $ function.embedding.subtype p

[PatrickMassot]

I know the name is similar, but I don't have a better idea. equiv.to_embedding has the right to use this name, and I didn't want to use a very long name. Suggestions are welcome.

[eric-wieser]

You're not a fan of the name equiv.embedding_of_subtype then?

[jcommelin]

It should be embedding_of_equiv_subtype then, right? I think equiv.as_embbeding is fine.
Also, sorry for kicking this on the queue. I missed that this conversation hadn't come to a conclusion yet.

[eric-wieser]

I figured the word equiv was redundant, hence dropping it from embedding_of_equiv_subtype.

Getting subtype in the name will probably make this more discoverable.

[jcommelin]

Thanks 🎉

bors merge

[jcommelin]

bors r-

(Still a conversation ongoing.)

[bors]

Canceled.

[eric-wieser]

Github marked #7037 (comment) as outdated, which discusses this name.

[eric-wieser]

Unrelated to the name conversation, we have some API to construct this:

Suggested change

	/-- Given an equivalence to a subtype, produce an embedding to the elements of the corresponding
	set. -/
	@[simps]
	def equiv.as_embedding {α β : Sort*} {p : β → Prop} (e : α ≃ subtype p) : α ↪ β :=
	⟨coe ∘ e, subtype.coe_injective.comp e.injective⟩
	/-- Given an equivalence to a subtype, produce an embedding to the elements of the corresponding
	set. -/
	@[simps]
	def equiv.as_embedding {α β : Sort*} {p : β → Prop} (e : α ≃ subtype p) : α ↪ β :=
	e.to_embedding.trans $ function.embedding.subtype p

which may or may not break the proof below.

[PatrickMassot]

I think it would be much faster if @eric-wieser could directly push to this branch. I really don't care at all, I simply want this in order to do interesting linear algebra with them. Any variation will be good enough for me.

[eric-wieser]

I didn't want to tread on your toes, and was waiting for a second opinion on the name. @jcommelin, if you pick a name I'll happily push to the branch

[jcommelin]

I understand the benefit of having subtype in the name. But I still find the proposal unnatural. It sounds like we are assuming some (x : subtype p).
So I suggest we just leave it as it is.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests