Set family operations #
This file defines a few binary operations on Set α
for use in set family combinatorics.
Main declarations #
s ⊻ t
: Set of elements of the forma ⊔ b
wherea ∈ s
,b ∈ t
.s ⊼ t
: Set of elements of the forma ⊓ b
wherea ∈ s
,b ∈ t
.
Notation #
We define the following notation in locale SetFamily
:
s ⊻ t
s ⊼ t
References #
[B. Bollobás, Combinatorics][bollobas1986]
s ⊻ t
is the set of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
.
Instances For
@[simp]
theorem
Set.sups_nonempty
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊻ t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.sups
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ⊻ t)
theorem
Set.Nonempty.of_sups_left
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊻ t) → Set.Nonempty s
theorem
Set.Nonempty.of_sups_right
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊻ t) → Set.Nonempty t
@[simp]
@[simp]
theorem
Set.image_sups
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[SemilatticeSup α]
[SemilatticeSup β]
[SupHomClass F α β]
(f : F)
(s : Set α)
(t : Set α)
:
@[simp]
@[simp]
theorem
Set.image_sup_prod
{α : Type u_2}
[SemilatticeSup α]
(s : Set α)
(t : Set α)
:
Set.image2 (fun x x_1 => x ⊔ x_1) s t = s ⊻ t
s ⊼ t
is the set of elements of the form a ⊓ b
where a ∈ s
, b ∈ t
.
Instances For
@[simp]
theorem
Set.infs_nonempty
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊼ t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.infs
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{t : Set α}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ⊼ t)
theorem
Set.Nonempty.of_infs_left
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊼ t) → Set.Nonempty s
theorem
Set.Nonempty.of_infs_right
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{t : Set α}
:
Set.Nonempty (s ⊼ t) → Set.Nonempty t
@[simp]
@[simp]
theorem
Set.image_infs
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[SemilatticeInf α]
[SemilatticeInf β]
[InfHomClass F α β]
(f : F)
(s : Set α)
(t : Set α)
:
@[simp]
@[simp]
theorem
Set.image_inf_prod
{α : Type u_2}
[SemilatticeInf α]
(s : Set α)
(t : Set α)
:
Set.image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
@[simp]
theorem
upperClosure_sups
{α : Type u_2}
[SemilatticeSup α]
(s : Set α)
(t : Set α)
:
upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t
@[simp]
theorem
lowerClosure_infs
{α : Type u_2}
[SemilatticeInf α]
(s : Set α)
(t : Set α)
:
lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t