leanprover-community / mathlib

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

Zulip Chat Archive

Stream: general

Topic: Projection maps out of and


Kind Bubble (Nov 29 2022 at 01:25):

Say p and q are propositions:

variable {p : Prop}
variable {q : Prop}

I couldn't figure out from the tutorial how to obtain these implications:

? : p \wedge q -> p
? : p \wedge q -> q

Eric Rodriguez (Nov 29 2022 at 01:36):

docs#and.left, docs#and.right


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll