Nonempty finite chains in a partially ordered type

Given a partially ordered type X, we introduce the type NonemptyFiniteChains of nonempty finite chains in X, i.e. nonempty finite subsets A of X such that all the elements in A are comparable.

structure PartialOrder.NonemptyFiniteChains (X : Type u) [PartialOrder X] : Type u

Given a partially ordered type X, this is the type of nonempty finite subsets A of X such that all the elements of A are comparable.

• finset : Finset X

  a finite subset

• nonempty : self.finset.Nonempty
• comparable (a b : ↥self.finset) : a ≤ b ∨ b ≤ a

theorem PartialOrder.NonemptyFiniteChains.ext {X : Type u} {inst✝ : PartialOrder X} {x y : NonemptyFiniteChains X} (finset : x.finset = y.finset) : x = y

theorem PartialOrder.NonemptyFiniteChains.ext_iff {X : Type u} {inst✝ : PartialOrder X} {x y : NonemptyFiniteChains X} : x = y ↔ x.finset = y.finset

@[implicit_reducible]

instance PartialOrder.NonemptyFiniteChains.inst (X : Type u) [PartialOrder X] : PartialOrder (NonemptyFiniteChains X)

Equations

• PartialOrder.NonemptyFiniteChains.inst X = PartialOrder.lift PartialOrder.NonemptyFiniteChains.finset ⋯

@[simp]

theorem PartialOrder.NonemptyFiniteChains.le_iff {X : Type u_1} [PartialOrder X] (A B : NonemptyFiniteChains X) : A ≤ B ↔ A.finset ≤ B.finset

@[simp]

theorem PartialOrder.NonemptyFiniteChains.lt_iff {X : Type u_1} [PartialOrder X] (A B : NonemptyFiniteChains X) : A < B ↔ A.finset < B.finset

noncomputable def PartialOrder.NonemptyFiniteChains.map {X : Type u_1} {Y : Type u_2} [PartialOrder X] [PartialOrder Y] (s : NonemptyFiniteChains X) (f : X →o Y) : NonemptyFiniteChains Y

The image of a nonempty finite chain by a monotone map.

Equations

• s.map f = { finset := Finset.image (⇑f) s.finset, nonempty := ⋯, comparable := ⋯ }

@[simp]

theorem PartialOrder.NonemptyFiniteChains.mem_map_iff {X : Type u_1} {Y : Type u_2} [PartialOrder X] [PartialOrder Y] (s : NonemptyFiniteChains X) (f : X →o Y) (y : Y) : y ∈ (s.map f).finset ↔ ∃ x ∈ s.finset, f x = y

noncomputable def PartialOrder.NonemptyFiniteChains.orderHomMap {X : Type u_1} {Y : Type u_2} [PartialOrder X] [PartialOrder Y] (f : X →o Y) : NonemptyFiniteChains X →o NonemptyFiniteChains Y

The monotone map NonemptyFiniteChains X →o NonemptyFiniteChains Y that is induced by f : X →o Y.

Equations

• PartialOrder.NonemptyFiniteChains.orderHomMap f = { toFun := fun (s : PartialOrder.NonemptyFiniteChains X) => s.map f, monotone' := ⋯ }

@[simp]

theorem PartialOrder.NonemptyFiniteChains.orderHomMap_coe {X : Type u_1} {Y : Type u_2} [PartialOrder X] [PartialOrder Y] (f : X →o Y) (s : NonemptyFiniteChains X) : (orderHomMap f) s = s.map f

noncomputable def PartOrd.nonemptyFiniteChainsFunctor : CategoryTheory.Functor PartOrd PartOrd

The functor PartOrd ⥤ PartOrd which sends a partially ordered type X to NonemptyFiniteChains X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PartOrd.nonemptyFiniteChainsFunctor_obj_coe (X : PartOrd) : ↑(nonemptyFiniteChainsFunctor.obj X) = PartialOrder.NonemptyFiniteChains ↑X

@[simp]

theorem PartOrd.nonemptyFiniteChainsFunctor_map {X✝ Y✝ : PartOrd} (f : X✝ ⟶ Y✝) : nonemptyFiniteChainsFunctor.map f = ofHom (PartialOrder.NonemptyFiniteChains.orderHomMap (Hom.hom f))