all-or-nothing sets

Stream: mathlib4

[Aaron Liu]

What should be the preferred way to express that a set s is all-or-nothing? I'm thinking either some variation on either s = ∅ ∨ s = univ or ∀ x ∈ s, ∀ y, y ∈ s. The advantage of the first way is that it's closer to what people actually say and the advantage of the second way is that it's easier to work with and prove things with.

[Yaël Dillies]

The former is what we use in results about the trivial sigma-algebra

[Aaron Liu]

I think the only time I've seen this second way being used is in docs#ComputablePred.rice

[Aaron Liu]

But I realized it's much easier to use this definition to, for example, define the indiscrete topology

[Michael Stoll]

grind can prove their equivalence, so it probably doesn't matter too much which one is used.

[Matt Diamond]

For the record, it's used the second way in ComputablePred.rice out of necessity, since it's a theorem about discriminating between Nat.Partrec functions but the type of the set is Set (ℕ →. ℕ) which includes non-partial-recursive functions. In that context, it actually wouldn't be accurate to say that the set is either empty or univ, since it could have some random non-p.r. functions. (Compare with docs#ComputablePred.rice₂, which involves a set of partrec codes and is stated in the first way.)

[Aaron Liu]

example proof

import Mathlib.Topology.Defs.Basic

example {α : Type u} : TopologicalSpace α where
  IsOpen s := ∀ ⦃x⦄, x ∈ s → ∀ y, y ∈ s
  isOpen_univ _ _ := Set.mem_univ
  isOpen_inter _ _ hs ht _ hx y := ⟨hs hx.1 y, ht hx.2 y⟩
  isOpen_sUnion _ h _ hx y :=
    (Set.mem_sUnion.1 hx).elim fun s hs => Set.mem_sUnion.2 ⟨s, hs.1, h s hs.1 hs.2 y⟩

[Trebor Huang]

This is also the constructively correct definition, incidentally

[Aaron Liu]

no wonder it's easier to work with