Set.Intersecting.insert
theorem Set.Intersecting.insert :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α},
s.Intersecting → a ≠ ⊥ → (∀ b ∈ s, ¬Disjoint a b) → (insert a s).Intersecting
The theorem `Set.Intersecting.insert` states that for any type `α` with a `SemilatticeInf` and `OrderBot` structure, a set `s` of type `α`, and an element `a` of type `α`, if `s` is an intersecting set (that is, every pair of elements in `s` is non-disjoint), `a` is not the bottom element, and `a` is not disjoint with any element in `s`, then the insertion of `a` into `s` results in a set that is still intersecting. In other words, adding an element that intersects with all the existing elements in an intersecting set maintains the intersecting property of the set.
More concisely: If `α` is a type with `SemilatticeInf` and `OrderBot` structures, `s` is an intersecting set of `α`, and `a` is not the bottom element nor disjoint with any element in `s`, then `a ∉ ∅ ∧ s ⊆ t ∧ ∀ x ∈ s, a ≤ x → a ∈ t` implies `a ∈ s ⊆ t`, where `t = s ∪ {a}`.
|
Set.Intersecting.isUpperSet'
theorem Set.Intersecting.isUpperSet' :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Finset α},
(↑s).Intersecting → (∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) → IsUpperSet ↑s
This theorem states that for any type `α` that forms a semilattice under an infimum operation and has a defined least element, and for any `s`, a finite set of elements of this type, if `s` is an intersecting family (its elements have a common intersection), and `s` is maximal with respect to being an intersecting family (i.e., there is no other intersecting family `t` that strictly contains `s`), then `s` is an upper set. In other words, if `a` and `b` are elements of type `α` such that `a` is less than or equal to `b` and `a` is in `s`, then `b` is also in `s`.
More concisely: If `α` is a semilattice with infimum and least element, `s` is a maximal intersecting finite subset of `α`, then `s` is an upper set.
|
Set.Intersecting.ne_bot
theorem Set.Intersecting.ne_bot :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α},
s.Intersecting → a ∈ s → a ≠ ⊥
This theorem states that for any type `α` that is both a semilattice (a partially ordered set with a greatest lower bound for any two elements) and an ordered set with a least element (`OrderBot`), if a set `s` of elements of `α` has the property that every two elements in it have non-disjoint intersection (i.e., they have a common element), then for any element `a` of this set, `a` cannot be the least element of the order (denoted by `⊥`). In other words, in such a set, the least element of the order is not included.
More concisely: In a semilattice with a least element where every pair of elements have non-empty intersection, no element is the least element.
|
Set.Intersecting.isUpperSet
theorem Set.Intersecting.isUpperSet :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α},
s.Intersecting → (∀ (t : Set α), t.Intersecting → s ⊆ t → s = t) → IsUpperSet s
This theorem states that for a given type `α` which has a semi-lattice infimum structure and a bottom element, any set `s` of this type that fulfills two properties is an upper set. The two properties are: first, `s` is an intersecting set, which means every pair of its elements has a non-empty intersection; second, `s` is maximal among intersecting sets, meaning that if `t` is another intersecting set of `α` and every element of `s` is also an element of `t`, then `s` and `t` must be the same set. In the context of order theory, an upper set is a set where if an element `a` is in the set and `a` is less than or equal to another element `b`, then `b` is also in the set.
More concisely: Given a type `α` with a semi-lattice infimum structure and a bottom element, any intersecting and maximal intersecting set `s` is an upper set in the order theory sense.
|