FiniteInter.inter_mem
theorem FiniteInter.inter_mem :
∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S := by
sorry
The theorem `inter_mem` asserts that for any type `α` and any set `S` of sets of `α`, if `S` is closed under finite intersections (i.e., `FiniteInter S`), then for any two sets `s` and `t` from `S` (denoted as `s ∈ S` and `t ∈ S`), their intersection (denoted as `s ∩ t`) is also in `S`. This emphasizes the closure property of a set of sets under the operation of intersection.
More concisely: If `S` is a set of sets of type `α` that is closed under finite intersections, then for all `s, t ∈ S`, we have `s ∩ t ∈ S`.
|
FiniteInter.univ_mem
theorem FiniteInter.univ_mem : ∀ {α : Type u_1} {S : Set (Set α)}, FiniteInter S → Set.univ ∈ S
The theorem `FiniteInter.univ_mem` asserts that for any type `α` and any set `S` of sets of `α`, if `S` is a finite intersection of sets, then the universal set on `α`, denoted as `Set.univ`, is an element of `S`. In other words, `Set.univ`, which contains all elements of type `α`, is included in the set `S` whenever `S` is the intersection of a finite number of sets.
More concisely: If `S` is a finite intersection of sets over type `α`, then `Set.univ ∊ S`.
|