Zulip Chat Archive

Stream: new members

Topic: How to apply this seemingly simple theorem in lean using con


guiwan (Jan 17 2025 at 18:33):

--The theorem can be described as follows:

Theorem Th1 (h1) (h2): [cs= ct, is= it, is ⊆ t ∧ t ⊆ cs].TFAE

--Here, "h1" and "h2" are conditions, "s" and "t" are sets, the corresponding notations "cs", "ct", "is", "it" are also sets. "TFAE" meas that the three terms in "[ ]" are equivalent.

--My goal: apply this Theorem to get the relations: when "h1" and "h2" are satisfied, "cs= ct" -> "cs= ct". ("->"means derive to)

Notification Bot (Jan 17 2025 at 21:59):

This topic was moved here from #rss > How to apply this seemingly simple theorem in lean using con by Kim Morrison.

Ruben Van de Velde (Jan 17 2025 at 22:00):

Please read #backticks and update your post accordingly


Last updated: May 02 2025 at 03:31 UTC