Zulip Chat Archive

Stream: new members

Topic: In a set


Martin Dvořák (Feb 27 2022 at 00:12):

I have a problem. When I was transforming it to MWE, a weird has_mem instance appeared, but here we are.

example (S : set ) (n : ) [has_mem  (  Prop)]
  (h : n  (λ (x : ), x  S)) :
    n  S :=
begin
  sorry,
end

Kevin Buzzard (Feb 27 2022 at 00:17):

[has_mem ℕ (ℕ → Prop)] means "let's decree that n \in (\lam x, x \in S) makes sense whilst attaching no meaning at all to it" so h is useless to you.

Martin Dvořák (Feb 27 2022 at 00:21):

Lemme make a less minimal example instead. Thanks for this observation!


Last updated: Dec 20 2023 at 11:08 UTC