Suggestion: Family Intersection World Level 6 / 6 : Intersection of a family of unions

[snoeyink]

Thanks for these exercises!

Just a suggestion spurred by
World: Family Intersection World
Level 6 / 6 : Intersection of a family of unions

We are asked to prove:
Suppose A is a set, F and G are families of sets, and for every set s in F, A∪s∈G. Then ⋂G⊆A∪(⋂F).

example (A : Set U) (F G : Set (Set U)) (h1 : ∀ s ∈ F, A ∪ s ∈ G) : ⋂₀ G ⊆ A ∪ (⋂₀ F)

Suggestion: Either the documentation of ⋂₀ could mention, or one of the earlier levels in this world could prove, that ⋂₀ F = U when F = {} is an empty family.

Justification: It seemed to me easiest to use by_cases hxF: x ∈ ⋂₀ F to prove this, but first I had to convince myself that this included the case where F was an empty family. The added proof early in this world would help students understand this special case of the possibly unfamiliar ⋂₀ operator.

Jack

[snoeyink]

Hmm... If I do it this way, however, then I want to use "obtain" because I get Exists t in F with x notin t, and that tactic is not unlocked yet. I'm curious what your proof is?

[djvelleman]

The text for this world suggests a different approach: by_cases hA : x ∈ A.

[djvelleman]

By the way, ⋂₀ F = U isn't quite right, because U is a type, not a set. What you mean is that ⋂₀ F is equal to the set of all objects of type U. This is the universal set for the type U, and the notation for it in Lean is Set.univ. So you could try this example in Lean:

import Mathlib.Order.SetNotation

example (U : Type) (F : Set (Set U)) (hFempty : F = {}) : ⋂₀ F = Set.univ