leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: to_Prop_inj


Kenny Lau (Jan 11 2019 at 10:31):

lemma to_Prop_inj : Π {a b : bool} (H : (a : Prop) ↔ (b : Prop)), a = b
| a tt H := H.2 rfl
| a ff H := bool.eq_ff_of_ne_tt $ λ h, absurd (H.1 h) dec_trivial

Kenny Lau (Jan 11 2019 at 10:31):

@Mario Carneiro is this currently in mathlib?


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll