left inverse

Stream: general

[Patrick Massot]

Today library_search is utterly failing me. Could it be true that we don't have:

lemma function.left_inverse_iff_comp {α β : Type*} (f : α → β) (g : β → α) : left_inverse f g ↔ f ∘ g = id :=
⟨λ h, funext $ h, λ h x, congr_fun h x

[Anne Baanen]

Looks like it is indeed missing. I see left_inverse.comp_eq_id in logic.function.basic but not the converse direction.

[Patrick Massot]

#3897

[Eric Wieser]

Is there a convention for when to provide separate lemmas for one or both directions of an iff vs just a single iff lemma?

[Anne Baanen]

I think that there should really only be the iff version, unless there is a strong argument that the implication is used a lot by itself (e.g. a typeclass is_foo defined as a structure with one field foo : Prop, then you might see both is_foo.foo and is_foo.iff_foo in use).

[Anne Baanen]

Often, a non-iff lemma sticks around if it was defined before the iff variant (as happened here).

[Eric Wieser]

Is there any kinda of deprecation process in place to allow removing weaker lemmas in situations like this? Perhaps a way to have lean emit a warning whenever a name is referred to?

[Anne Baanen]

Mathlib is aggressively backwards-incompatible, so the deprecation process is basically "delete the obsolete thing and fix any build error that occurs in the official repositories".

[Anne Baanen]

It should definitely be possible to make a linter to detect usages of deprecated definitions, like the linter that complains about usage of > where < would also work.

[Mario Carneiro]

You will find a lot of one-directional lemmas in theorems that originated in core lean (i.e. algebra.ordered_group and friends), because MS lean style is a bit different from mathlib style. Since these have moved to mathlib, they are being phased out.