## Stream: new members

### Topic: involution and ite

#### Yakov Pechersky (Sep 08 2020 at 20:29):

What would be the most mathlib-friendly way to state this? Is this too specific? What file would it go in?

import logic.function.basic

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α → α} (hinv : function.involutive f) (x : α) :
ite P x (f x) = f (ite (¬ P) x (f x)) :=
begin
rw apply_ite f,
by_cases h : P,
{ rw [if_pos h, if_neg (not_not.mpr h), hinv x] },
{ rw [if_pos h, if_neg h] },
end


#### Alex J. Best (Sep 08 2020 at 20:41):

adding a lemma ite_neg seems useful:

lemma ite_neg {c : Prop} {X : Type*} (a b : X) [decidable c] : ite (¬ c) a b = ite c b a :=
by split_ifs; refl

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α → α} (hinv : function.involutive f) (x : α) :
ite P x (f x) = f (ite (¬ P) x (f x)) :=
by rw [apply_ite f, hinv, ite_neg]


#### Kenny Lau (Sep 08 2020 at 20:50):

always generalize

#### Yakov Pechersky (Sep 08 2020 at 20:54):

So, PR this?

lemma ite_neg {c : Prop} {X : Type*} (a b : X) [decidable c] : ite (¬ c) a b = ite c b a :=
by split_ifs; refl

lemma inv_ite {α : Type*} (P : Prop) [decidable P] {f : α → α} (hinv : function.involutive f) (x : α) :
f (ite P x (f x)) = ite (¬ P) x (f x) :=
by rw [apply_ite f, hinv, ite_neg]


Sure!

#### Yakov Pechersky (Sep 08 2020 at 22:11):

#4074

Last updated: May 13 2021 at 22:15 UTC