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