Zulip Chat Archive

Stream: general

Topic: easy subset/subtype lemma


view this post on Zulip Kevin Buzzard (Jul 16 2018 at 14:15):

I've reduced my goal to

example (X : Type) (U A B : set X) : U  A = U  B  {u : U | u.val  A} = {u : U | u.val  B} := sorry

Is there a one-liner for this? As it happens I only need the <- direction but it somehow all looks easy.

view this post on Zulip Simon Hudon (Jul 16 2018 at 14:18):

can you try by ext; dsimp; tauto?

view this post on Zulip Simon Hudon (Jul 16 2018 at 14:19):

Sorry, no that won't work

view this post on Zulip Mario Carneiro (Jul 16 2018 at 14:20):

there should be a lemma {x : A | x \in B} = A \cap B

view this post on Zulip Mario Carneiro (Jul 16 2018 at 14:20):

wait, that's not type correct

view this post on Zulip Patrick Massot (Jul 16 2018 at 14:20):

hence Kevin's .val

view this post on Zulip Simon Hudon (Jul 16 2018 at 14:22):

Second attempt: dsimp [set_eq_def]; apply forall_congr; tauto

view this post on Zulip Mario Carneiro (Jul 16 2018 at 14:23):

I think and.congr_right needs a biconditional version

view this post on Zulip Mario Carneiro (Jul 16 2018 at 14:38):

lemma and.congr_right_iff {a b c : Prop} : (a  b  a  c)  (a  (b  c)) :=
⟨λ h ha, by simp [ha] at h; exact h, and_congr_right

example (X : Type) (U A B : set X) :
  U  A = U  B  {u : U | u.val  A} = {u : U | u.val  B} :=
by simp [set.set_eq_def, and.congr_right_iff]

view this post on Zulip Kevin Buzzard (Jul 16 2018 at 14:47):

Thanks Mario.

view this post on Zulip Kevin Buzzard (Jul 16 2018 at 14:50):

@Luca Gerolla is doing homotopy theory in Lean and this was all that was left for proving that a function on [0,1] is continuous iff its restriction to [0,1/2] and [1/2,1] is.


Last updated: May 08 2021 at 10:12 UTC