Set.mem_sUnion
theorem Set.mem_sUnion : ∀ {α : Type u} {x : α} {S : Set (Set α)}, x ∈ S.sUnion ↔ ∃ t ∈ S, x ∈ t
This theorem, `Set.mem_sUnion`, states that for all types `α`, and for all elements `x` of this type, and for all sets `S` of sets of `α`, the element `x` is a member of the union over all sets in `S` if and only if there exists a set `t` in `S` such that `x` is a member of `t`. This is equivalent to stating that an element belongs to the union of a collection of sets if it belongs to at least one of the sets in the collection.
More concisely: For any type `α` and sets `S` of sets of `α`, an element `x` is in the union of `S` if and only if it is in some set in `S`.
|
Mathlib.Order.SetNotation._auxLemma.4
theorem Mathlib.Order.SetNotation._auxLemma.4 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋂ i, s i) = ∀ (i : ι), x ∈ s i
This theorem states that for any type `α`, any index type `ι`, any element `x` of type `α`, and any indexed set `s` of elements of type `α`, the element `x` is a member of the intersection of all sets `s i` (for all `i` in `ι`) if and only if `x` is a member of each set `s i`. In mathematical terms, this can be represented as `x ∈ ⋂ i, s i` if and only if `∀ (i : ι), x ∈ s i`. Essentially, it formalizes the notion that an element belongs to the intersection of a collection of sets if and only if it belongs to each set in the collection.
More concisely: For any type `α`, index type `ι`, set `s` of elements of type `α`, and element `x` of type `α`, `x` is in the intersection of all sets `s i` (for all `i` in `ι`) if and only if `x` is an element of each set `s i`. Equivalently, `x ∈ ⋂ i, s i` if and only if `∀ (i : ι), x ∈ s i`.
|
Set.mem_iInter
theorem Set.mem_iInter : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, x ∈ ⋂ i, s i ↔ ∀ (i : ι), x ∈ s i := by
sorry
The theorem `Set.mem_iInter` states that for any type `α`, any index type `ι`, any element `x` of type `α`, and any function `s` from `ι` to the set of `α`, `x` is in the intersection over `i` of `s i` if and only if for every `i` in `ι`, `x` is in `s i`. In other words, an element belongs to the intersection of a collection of sets if and only if it belongs to each set in the collection.
More concisely: For any type `α`, index type `ι`, function `s` from `ι` to the sets over `α`, and `x` in `α`, `x` is in the intersection of `{s i | i ∈ ι}` if and only if `x` is in `s i` for all `i` in `ι`.
|
Mathlib.Order.SetNotation._auxLemma.3
theorem Mathlib.Order.SetNotation._auxLemma.3 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem states that for any type `α`, any sort `ι`, any element `x` of type `α`, and any function `s` that maps elements of sort `ι` to sets of type `α`, the statement "element `x` belongs to the union of sets `s i` for all `i`" is equivalent to the statement "there exists an `i` such that `x` belongs to the set `s i`". In mathematical terms, this is saying that $x \in \bigcup_{i} s_i$ is equivalent to $\exists i, x \in s_i$.
More concisely: For any type `α`, sort `ι`, element `x` of type `α`, and function `s` mapping `ι` to sets of `α`, $x \in \bigcup\_{i} s\_i$ if and only if there exists an `i`, such that $x \in s\_i$.
|
Set.mem_iUnion
theorem Set.mem_iUnion : ∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, x ∈ ⋃ i, s i ↔ ∃ i, x ∈ s i
This theorem `Set.mem_iUnion` states that for all types `α` and a sort `ι`, and for any element `x` of type `α` and a function `s` mapping `ι` to a set of `α`, the element `x` is in the union of all the sets defined by `s i` for all `i` if and only if there exists some `i` such that `x` is in the set `s i`. In simple words, an element belongs to the union of a collection of sets if and only if it belongs to at least one set in that collection.
More concisely: An element belongs to the union of a family of sets if and only if it is an element of at least one set in the family.
|