Order.PFilter.ext
theorem Order.PFilter.ext : ∀ {P : Type u_1} [inst : Preorder P] (s t : Order.PFilter P), ↑s = ↑t → s = t
This theorem states that for any type `P` that has a `Preorder` instance, two preorder filters `s` and `t` are equal if and only if their underlying sets are equal. In other words, if the set of elements contained in filter `s` is identical to the set of elements contained in filter `t`, then `s` equals `t`. This is a fundamental property of filters in the context of preordered sets.
More concisely: For any preordered type `P` with equal preorder filters `s` and `t`, their underlying sets equal imply `s = t`.
|
Order.PFilter.inf_mem
theorem Order.PFilter.inf_mem :
∀ {P : Type u_1} [inst : SemilatticeInf P] {x y : P} {F : Order.PFilter P}, x ∈ F → y ∈ F → x ⊓ y ∈ F
This theorem states that for any type `P` which forms a semilattice with the inf (meet) operation, given any `x` and `y` in `P` and any filter `F` on `P`, if both `x` and `y` are elements of `F`, then their meet (`x` inf `y`) is also an element of `F`. This provides a specific witness of the `pfilter.directed` property when `P` has meets. In simpler terms, it asserts that in a certain kind of ordered structure, the meet of any two elements in a filter is also in the filter.
More concisely: In a semilattice with meets, if two elements belong to a filter, then their meet also belongs to the filter.
|
Order.PFilter.top_mem
theorem Order.PFilter.top_mem :
∀ {P : Type u_1} [inst : Preorder P] [inst_1 : OrderTop P] {F : Order.PFilter P}, ⊤ ∈ F
This theorem states that for any type `P` with a preorder and a greatest element (often denoted by '⊤'), and for any `PFilter` (which is a filter on the preorder `P`), the greatest element '⊤' is an element of the `PFilter`. Essentially, the greatest element is always part of such a filter, no matter which specific filter we're talking about.
More concisely: For any preorder type `P` with a greatest element `⊤`, and any filter `PFilter` on `P`, the greatest element `⊤` belongs to the filter `PFilter`.
|