The upper-set cube above a finite antichain

noncomputable def MagnitudeConjecture.AntichainUpperCube.base {T : Type u} [PartialOrder T] [Fintype T] (A : Finset T) : Finset T

Elements strictly above at least one member of the antichain.

@[simp]

theorem MagnitudeConjecture.AntichainUpperCube.mem_base {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A : Finset T) (t : T) : t ∈ base A ↔ ∃ a ∈ A, a < t

theorem MagnitudeConjecture.AntichainUpperCube.base_isUpperSet {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A : Finset T) : IsUpperSet ↑(base A)

The strict upper part is an upper set.

theorem MagnitudeConjecture.AntichainUpperCube.base_disjoint {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A : Finset T) (hA : ∀ a ∈ A, ∀ b ∈ A, a ≤ b → a = b) : Disjoint (base A) A

The strict upper part contains no member of the antichain.

theorem MagnitudeConjecture.AntichainUpperCube.union_isUpperSet {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A B : Finset T) (hB : B ⊆ A) : IsUpperSet ↑(base A ∪ B)

Adjoining any subset of the antichain to the strict upper part gives an upper set.

theorem MagnitudeConjecture.AntichainUpperCube.card_union {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A B : Finset T) (hA : ∀ a ∈ A, ∀ b ∈ A, a ≤ b → a = b) (hB : B ⊆ A) : (base A ∪ B).card = (base A).card + B.card

The cube vertex indexed by B has exactly |B| more elements than its base.

theorem MagnitudeConjecture.AntichainUpperCube.union_injective {T : Type u} [PartialOrder T] [Fintype T] [DecidableEq T] (A : Finset T) (hA : ∀ a ∈ A, ∀ b ∈ A, a ≤ b → a = b) {B C : Finset T} (hB : B ⊆ A) (hC : C ⊆ A) (heq : base A ∪ B = base A ∪ C) : B = C

Different subsets of the antichain give different cube vertices.