Set family operations #
This file defines a few binary operations on Finset α
for use in set family combinatorics.
Main declarations #
s ⊻ t
: Finset of elements of the forma ⊔ b
wherea ∈ s
,b ∈ t
.s ⊼ t
: Finset of elements of the forma ⊓ b
wherea ∈ s
,b ∈ t
.Finset.disjSups s t
: Finset of elements of the forma ⊔ b
wherea ∈ s
,b ∈ t
anda
andb
are disjoint.
Notation #
We define the following notation in locale FinsetFamily
:
s ⊻ t
s ⊼ t
s ○ t
forFinset.disjSups s t
References #
[B. Bollobás, Combinatorics][bollobas1986]
s ⊻ t
is the finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
.
Instances For
@[simp]
theorem
Finset.coe_sups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.card_sups_le
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ⊻ t) ≤ Finset.card s * Finset.card t
theorem
Finset.card_sups_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ⊻ t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun x => x.fst ⊔ x.snd) (↑s ×ˢ ↑t)
theorem
Finset.sup_mem_sups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
{a : α}
{b : α}
:
theorem
Finset.sups_subset
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.sups_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.sups_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.image_subset_sups_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
{b : α}
:
b ∈ t → Finset.image (fun a => a ⊔ b) s ⊆ s ⊻ t
theorem
Finset.image_subset_sups_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
{a : α}
:
a ∈ s → Finset.image (fun x => a ⊔ x) t ⊆ s ⊻ t
theorem
Finset.forall_sups_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
{p : α → Prop}
:
@[simp]
theorem
Finset.sups_subset_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
{u : Finset α}
:
@[simp]
theorem
Finset.sups_nonempty
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊻ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t
theorem
Finset.Nonempty.sups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s ⊻ t)
theorem
Finset.Nonempty.of_sups_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊻ t) → Finset.Nonempty s
theorem
Finset.Nonempty.of_sups_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊻ t) → Finset.Nonempty t
@[simp]
@[simp]
@[simp]
theorem
Finset.singleton_sups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{t : Finset α}
{a : α}
:
{a} ⊻ t = Finset.image (fun b => a ⊔ b) t
@[simp]
theorem
Finset.sups_singleton
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{b : α}
:
s ⊻ {b} = Finset.image (fun a => a ⊔ b) s
theorem
Finset.singleton_sups_singleton
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{a : α}
{b : α}
:
theorem
Finset.sups_union_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.sups_union_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.sups_inter_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.sups_inter_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.biUnion_image_sup_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
(Finset.biUnion s fun a => Finset.image ((fun x x_1 => x ⊔ x_1) a) t) = s ⊻ t
theorem
Finset.biUnion_image_sup_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
(Finset.biUnion t fun b => Finset.image (fun a => a ⊔ b) s) = s ⊻ t
theorem
Finset.image_sup_product
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
Finset.image (Function.uncurry fun x x_1 => x ⊔ x_1) (s ×ˢ t) = s ⊻ t
theorem
Finset.sups_assoc
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.sups_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.sups_left_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.sups_right_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
s ⊼ t
is the finset of elements of the form a ⊓ b
where a ∈ s
, b ∈ t
.
Instances For
@[simp]
theorem
Finset.coe_infs
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.card_infs_le
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ⊼ t) ≤ Finset.card s * Finset.card t
theorem
Finset.card_infs_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
Finset.card (s ⊼ t) = Finset.card s * Finset.card t ↔ Set.InjOn (fun x => x.fst ⊓ x.snd) (↑s ×ˢ ↑t)
theorem
Finset.inf_mem_infs
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
{a : α}
{b : α}
:
theorem
Finset.infs_subset
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.infs_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.infs_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.image_subset_infs_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
{b : α}
:
b ∈ t → Finset.image (fun a => a ⊓ b) s ⊆ s ⊼ t
theorem
Finset.image_subset_infs_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
{a : α}
:
a ∈ s → Finset.image (fun x => a ⊓ x) t ⊆ s ⊼ t
theorem
Finset.forall_infs_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
{p : α → Prop}
:
@[simp]
theorem
Finset.infs_subset_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
{u : Finset α}
:
@[simp]
theorem
Finset.infs_nonempty
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊼ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t
theorem
Finset.Nonempty.infs
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty s → Finset.Nonempty t → Finset.Nonempty (s ⊼ t)
theorem
Finset.Nonempty.of_infs_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊼ t) → Finset.Nonempty s
theorem
Finset.Nonempty.of_infs_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (s ⊼ t) → Finset.Nonempty t
@[simp]
@[simp]
@[simp]
theorem
Finset.singleton_infs
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{t : Finset α}
{a : α}
:
{a} ⊼ t = Finset.image (fun b => a ⊓ b) t
@[simp]
theorem
Finset.infs_singleton
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{b : α}
:
s ⊼ {b} = Finset.image (fun a => a ⊓ b) s
theorem
Finset.singleton_infs_singleton
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{a : α}
{b : α}
:
theorem
Finset.infs_union_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.infs_union_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.infs_inter_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
theorem
Finset.infs_inter_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
theorem
Finset.biUnion_image_inf_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
(Finset.biUnion s fun a => Finset.image ((fun x x_1 => x ⊓ x_1) a) t) = s ⊼ t
theorem
Finset.biUnion_image_inf_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
(Finset.biUnion t fun b => Finset.image (fun a => a ⊓ b) s) = s ⊼ t
theorem
Finset.image_inf_product
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
Finset.image (Function.uncurry fun x x_1 => x ⊓ x_1) (s ×ˢ t) = s ⊼ t
theorem
Finset.infs_assoc
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.infs_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
:
theorem
Finset.infs_left_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.infs_right_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeInf α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.sups_infs_subset_left
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.sups_infs_subset_right
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.infs_sups_subset_left
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
theorem
Finset.infs_sups_subset_right
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
def
Finset.disjSups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
:
Finset α
The finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
and a
and b
are disjoint.
Instances For
The finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
and a
and b
are disjoint.
Instances For
@[simp]
theorem
Finset.mem_disjSups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
{c : α}
:
theorem
Finset.disjSups_subset_sups
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
:
Finset.disjSups s t ⊆ s ⊻ t
theorem
Finset.card_disjSups_le
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
:
Finset.card (Finset.disjSups s t) ≤ Finset.card s * Finset.card t
theorem
Finset.disjSups_subset
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s₁ : Finset α}
{s₂ : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(hs : s₁ ⊆ s₂)
(ht : t₁ ⊆ t₂)
:
Finset.disjSups s₁ t₁ ⊆ Finset.disjSups s₂ t₂
theorem
Finset.disjSups_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
(ht : t₁ ⊆ t₂)
:
Finset.disjSups s t₁ ⊆ Finset.disjSups s t₂
theorem
Finset.disjSups_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
(hs : s₁ ⊆ s₂)
:
Finset.disjSups s₁ t ⊆ Finset.disjSups s₂ t
theorem
Finset.forall_disjSups_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
{p : α → Prop}
:
@[simp]
theorem
Finset.disjSups_subset_iff
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
{u : Finset α}
:
theorem
Finset.Nonempty.of_disjSups_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (Finset.disjSups s t) → Finset.Nonempty s
theorem
Finset.Nonempty.of_disjSups_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t : Finset α}
:
Finset.Nonempty (Finset.disjSups s t) → Finset.Nonempty t
@[simp]
theorem
Finset.disjSups_empty_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{t : Finset α}
:
Finset.disjSups ∅ t = ∅
@[simp]
theorem
Finset.disjSups_empty_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
:
Finset.disjSups s ∅ = ∅
theorem
Finset.disjSups_singleton
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{a : α}
{b : α}
:
Finset.disjSups {a} {b} = if Disjoint a b then {a ⊔ b} else ∅
theorem
Finset.disjSups_union_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
Finset.disjSups (s₁ ∪ s₂) t = Finset.disjSups s₁ t ∪ Finset.disjSups s₂ t
theorem
Finset.disjSups_union_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
Finset.disjSups s (t₁ ∪ t₂) = Finset.disjSups s t₁ ∪ Finset.disjSups s t₂
theorem
Finset.disjSups_inter_subset_left
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s₁ : Finset α}
{s₂ : Finset α}
{t : Finset α}
:
Finset.disjSups (s₁ ∩ s₂) t ⊆ Finset.disjSups s₁ t ∩ Finset.disjSups s₂ t
theorem
Finset.disjSups_inter_subset_right
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
{s : Finset α}
{t₁ : Finset α}
{t₂ : Finset α}
:
Finset.disjSups s (t₁ ∩ t₂) ⊆ Finset.disjSups s t₁ ∩ Finset.disjSups s t₂
theorem
Finset.disjSups_comm
{α : Type u_1}
[DecidableEq α]
[SemilatticeSup α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
:
Finset.disjSups s t = Finset.disjSups t s
theorem
Finset.disjSups_assoc
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
Finset.disjSups (Finset.disjSups s t) u = Finset.disjSups s (Finset.disjSups t u)
theorem
Finset.disjSups_left_comm
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
Finset.disjSups s (Finset.disjSups t u) = Finset.disjSups t (Finset.disjSups s u)
theorem
Finset.disjSups_right_comm
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
(u : Finset α)
:
Finset.disjSups (Finset.disjSups s t) u = Finset.disjSups (Finset.disjSups s u) t
theorem
Finset.disjSups_disjSups_disjSups_comm
{α : Type u_1}
[DecidableEq α]
[DistribLattice α]
[OrderBot α]
[DecidableRel Disjoint]
(s : Finset α)
(t : Finset α)
(u : Finset α)
(v : Finset α)
:
Finset.disjSups (Finset.disjSups s t) (Finset.disjSups u v) = Finset.disjSups (Finset.disjSups s u) (Finset.disjSups t v)