Zulip Chat Archive

Stream: general

Topic: does lean know?

Sean Leather (Mar 01 2018 at 09:46):

Is this in the standard library or mathlib?

theorem if_distrib {c : Prop} [decidable c] {α β : Type} {f : α  β} {a b : α}:
  f (if c then a else b) = if c then f a else f b :=
by by_cases h : c; [simp [if_pos h], simp [if_neg h]]

Sean Leather (Mar 01 2018 at 09:48):

@Kenny Lau: FYI, the topic title is in homage to your questions. :simple_smile:

Kenny Lau (Mar 01 2018 at 09:48):


Last updated: Aug 03 2023 at 10:10 UTC