function properties

Stream: new members

[Holly Liu]

/-- A function is involutive, if `f ∘ f = id`. -/
def involutive {α} (f : α → α) : Prop := ∀ x, f (f x) = x

lemma involutive_iff_iter_2_eq_id {α} {f : α → α} : involutive f ↔ (f^[2] = id) :=
funext_iff.symm

namespace involutive
variables {α : Sort u} {f : α → α} (h : involutive f)
include h

@[simp]
lemma comp_self : f ∘ f = id := funext h

protected lemma left_inverse : left_inverse f f := h
protected lemma right_inverse : right_inverse f f := h

protected lemma injective : injective f := h.left_inverse.injective
protected lemma surjective : surjective f := λ x, ⟨f x, h x⟩
protected lemma bijective : bijective f := ⟨h.injective, h.surjective⟩

i'm confused on why lemmas like protected lemma injective : injective f := h.left_inverse.injective are allowed to use injective in the name of the lemma, the proof goal, and the proof itself? is injectivealso defined elsewhere?

[Eric Wieser]

Yes, docs#function.injective

[Eric Wieser]

Hovering over the name in vscode should tell you that

[Eric Wieser]

Or failing that, right clicking and saying "go to definition"

[Holly Liu]

thanks. yes, i am able to see the definition by hovering, although "go to definition" doesn't yield anything for me. i'm searching the github files which doesn't have those mechanisms.

[Yakov Pechersky]

The word after "lemma" is the name for the lemma. It can be basically anything. "protected" means it will be named "involutive.injective", because we are in the "involutive" namespace, and even if someone did "open involutive". The second "injective" refers to "function.injective". It can't refer to the "injective" we just named, because that is only available (when proving in this fashion) after our proof. The third injective is from "left_injective.injective", which is the lemma that states that given a hypothesis that some function is a "left_inverse", then it means the function discussed is injective.

[Holly Liu]

thanks for the reply! could you elaborate on left_inverse.injective? are you referring to protected lemma left_inverse : left_inverse f f := h and if so, does appending a .inverse to this function (left_inverse.injective) make it the injective property related to left_inverse ?

[Kevin Buzzard]

docs#function.left_inverse.injective

[Kevin Buzzard]

It's that.

[Holly Liu]

so is h.left_inverse.injective equivalent to left_inverse.injective h?

[Yakov Pechersky]

Yes, as long as you have "open function"

[Yakov Pechersky]

It's not just equivalent, it is literally the same.