Should these go into mathlib?

Stream: maths

[Marc Masdeu]

Hi,

I am going through a for_mathlib.lean file and have found these two candidates. They came as a surprise to me, since I thought (after reading the Xena blog posts of @Kevin Buzzard) that sets were just a notation for propositional logic (I don't really know if I'm saying something sensible here). Should I PR them? They'll need to be golfed through, though...

@[simp]
lemma set.univ_iff {α : Type} (p : α → Prop) : {x : α | p x} = univ ↔ ∀ x, p x :=
begin
  split,
  { intros h x,
    have h1 := mem_univ x,
    rw ← h at h1,
    exact h1 },
  { intros h,
    ext,
    simp only [mem_univ, mem_set_of_eq, iff_true],
    exact h x }
end

@[simp]
lemma set.empty_iff {α : Type} {p : α → Prop} : {x : α | p x} = ∅ ↔ ∀ x, ¬ p x :=
begin
  split,
  { intros h x,
    have h1 := mem_empty_eq x,
    rw ← h at h1,
    norm_num at h1 },
  { intros h,
    ext,
    norm_num,
    exact h x }
end

[Johan Commelin]

there is docs#set.eq_univ_iff_forall

[Johan Commelin]

Marc Masdeu said:

I am going through a for_mathlib.lean file and have found these two candidates. They came as a surprise to me, since I thought (after reading the Xena blog posts of Kevin Buzzard) that sets were just a notation for propositional logic (I don't really know if I'm saying something sensible here).

This is true technically, set X := X -> Prop. But in practice there is an API barrier between the two which shouldn't be breached by force. So the type of lemmas that you propose are good ones.
On the other hand, I think they can be proved by combining 2 or 3 existing lemmas from the library. You should need at most 2 lines for the proof.

[Marc Masdeu]

Oh wow! So the first lemmas is proven by simpa using set.eq_univ_iff_forall! It turns out that library_search wasn't very helpful there.

[Johan Commelin]

For the other one, I guess docs#set.eq_empty_iff_forall_not_mem should help

[Marc Masdeu]

@[simp]
lemma set.univ_iff {α : Type} (p : α → Prop) : {x : α | p x} = univ ↔ ∀ x, p x :=
by simpa using set.eq_univ_iff_forall

@[simp]
lemma set.empty_iff {α : Type} {p : α → Prop} : {x : α | p x} = ∅ ↔ ∀ x, ¬ p x :=
by simpa using set.eq_empty_iff_forall_not_mem

[Marc Masdeu]

Johan Commelin said:

For the other one, I guess docs#set.eq_empty_iff_forall_not_mem should help

Yes, I managed to find this one by myself :smile:

[Marc Masdeu]

Since we are here, what about this one? Is there a lemma that is essentially this?

lemma sUnion_eq_of_pointwise {X : Type} {U : set X} {ℬ : set (set X)} :
  ( ∃ J ⊆ ℬ, U = ⋃₀ J ) ↔  (∀ x ∈ U, ∃ W ∈ ℬ, x ∈ W ∧ W ⊆ U) :=
begin
  split,
  { intros h x hx,
    obtain ⟨J, ⟨hJ1, hJ2⟩⟩ := h,
    subst hJ2,
    rw mem_sUnion at hx,
    obtain ⟨t, ht1, ht2⟩ := hx,
    use t,
    repeat {split},
    { tauto },
    { tauto },
    { exact subset_sUnion_of_mem ht1 } },
  { intro h,
    use {W ∈ ℬ | W ⊆ U},
    split,
    { apply sep_subset },
    apply eq_of_subset_of_subset,
    all_goals {intros x hx, simp at hx ⊢, try {specialize h x hx}, tauto } }
end

[Eric Wieser]

Two other ways to get there:

-- sneaky unfolding
@[simp]
lemma set.univ_iff₁ {α : Type} (p : α → Prop) : {x : α | p x} = set.univ ↔ ∀ x, p x :=
set.eq_univ_iff_forall

-- rewrites
@[simp]
lemma set.univ_iff₂ {α : Type} (p : α → Prop) : {x : α | p x} = set.univ ↔ ∀ x, p x :=
by simp_rw [set.eq_univ_iff_forall, set.mem_set_of_eq]

[Eric Wieser]

I suspect there are some lemmas about ⋃₀ and set.sep that are probably missing - try splitting your proof of sUnion_eq_of_pointwise into smaller pieces, and see if mathlib has analogues for some of them

[Marc Masdeu]

I see, so really they "are" in mathlib, up to this weird unfolding. Funny that there is a lemma in mathlib that closes the goal, but at the same time library_search doesn't find it.

[Eric Wieser]

Golfed a little:

lemma sUnion_eq_of_pointwise {X : Type} {U : set X} {ℬ : set (set X)} :
  ( ∃ J ⊆ ℬ, U = ⋃₀ J ) ↔  (∀ x ∈ U, ∃ W ∈ ℬ, x ∈ W ∧ W ⊆ U) :=
begin
  split,
  { rintros ⟨J, hJ1, rfl⟩ x ⟨t, ht1, ht2⟩,
    exact ⟨t, hJ1 ht1, ht2, subset_sUnion_of_mem ht1⟩, },
  { intro h,
    refine ⟨{W ∈ ℬ | W ⊆ U}, sep_subset _ _, _⟩,
    apply eq_of_subset_of_subset,
    { intros x hx,
      obtain ⟨W, hWB, hXw, hwu⟩ := h x hx,
      exact ⟨W, ⟨hWB, hwu⟩, hXw⟩, },
    { rintros x ⟨W, ⟨-, hWU⟩, hXw⟩,
      exact hWU hXw, }, }
end

[Marc Masdeu]

Great! What I like about this lemma is that the RHS doesn't mention J.