Filter.mem_zero
theorem Filter.mem_zero : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, s ∈ 0 ↔ 0 ∈ s
This is a theorem about filters in the context of a set theory. Specifically, the theorem states that for any type `α` that has a zero element (denoted by the `Zero α` instance), and any set `s` of elements of type `α`, the set `s` is an element of the zero filter if and only if the zero element is an element of the set `s`. In other words, the zero filter contains a set if and only if that set contains the zero element.
More concisely: For any set `s` of type `α` with a zero element, `s` is in the zero filter if and only if `Zero α` is in `s`.
|
Filter.mem_one
theorem Filter.mem_one : ∀ {α : Type u_2} [inst : One α] {s : Set α}, s ∈ 1 ↔ 1 ∈ s
This theorem, `Filter.mem_one`, states that for any type `α` which has a `One` instance (that is, an instance of the multiplicative identity `1`), and any set `s` of elements of type `α`, `s` belongs to `1` if and only if `1` belongs to `s`. In other words, the membership of the set `s` in `1` is equivalent to the membership of `1` in the set `s`. This is a statement about the symmetry of membership between the multiplicative identity and any set of elements of a type that supports the concept of the multiplicative identity.
More concisely: For any type `α` with a `One` instance and set `s` of elements from `α`, `1 ∈ s` if and only if `s ∈ 1`.
|