Set family operations #
This file defines a few binary operations on Finset α
for use in set family combinatorics.
Main declarations #
Finset.sups s t
: Finset of elements of the forma ⊔ b
wherea ∈ s
,b ∈ t
.Finset.infs 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.Finset.diffs
: Finset of elements of the forma \ b
wherea ∈ s
,b ∈ t
.Finset.compls
: Finset of elements of the formaᶜ
wherea ∈ s
.
Notation #
We define the following notation in locale FinsetFamily
:
s ⊻ t
forFinset.sups
s ⊼ t
forFinset.infs
s ○ t
forFinset.disjSups s t
s \\ t
forFinset.diffs
sᶜˢ
forFinset.compls
References #
s ⊻ t
is the finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
.
Equations
- Finset.hasSups = { sups := Finset.image₂ fun (x1 x2 : α) => x1 ⊔ x2 }
Instances For
s ⊼ t
is the finset of elements of the form a ⊓ b
where a ∈ s
, b ∈ t
.
Equations
- Finset.hasInfs = { infs := Finset.image₂ fun (x1 x2 : α) => x1 ⊓ x2 }
Instances For
The finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
and a
and b
are disjoint.
Equations
- s.disjSups t = Finset.image (fun (ab : α × α) => ab.1 ⊔ ab.2) (Finset.filter (fun (ab : α × α) => Disjoint ab.1 ab.2) (s ×ˢ t))
Instances For
The finset of elements of the form a ⊔ b
where a ∈ s
, b ∈ t
and a
and b
are disjoint.
Equations
- FinsetFamily.«term_○_» = Lean.ParserDescr.trailingNode `FinsetFamily.term_○_ 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 75))
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
s \\ t
is the finset of elements of the form a \ b
where a ∈ s
, b ∈ t
.
Equations
- Finset.diffs = Finset.image₂ fun (x1 x2 : α) => x1 \ x2
Instances For
s \\ t
is the finset of elements of the form a \ b
where a ∈ s
, b ∈ t
.
Equations
- FinsetFamily.«term_\\_» = Lean.ParserDescr.trailingNode `FinsetFamily.term_\\_ 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\\\ ") (Lean.ParserDescr.cat `term 75))
Instances For
sᶜˢ
is the finset of elements of the form aᶜ
where a ∈ s
.
Equations
- Finset.compls = Finset.map { toFun := compl, inj' := ⋯ }
Instances For
sᶜˢ
is the finset of elements of the form aᶜ
where a ∈ s
.
Equations
- FinsetFamily.«term_ᶜˢ» = Lean.ParserDescr.trailingNode `FinsetFamily.term_ᶜˢ 1024 1024 (Lean.ParserDescr.symbol "ᶜˢ")
Instances For
Alias of the reverse direction of Finset.compls_nonempty
.
Alias of the forward direction of Finset.compls_nonempty
.