def OmegaCompletePartialOrder.Chain.Sigma.inj {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] {i : I} (c : Chain (P i)) : Chain ((i : I) × P i)

Injects a chain into a chain of coproducts.

Equations

• OmegaCompletePartialOrder.Chain.Sigma.inj c = { toFun := fun (n : ℕ) => ⟨i, c n⟩, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sigma.inj_coe {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] {i : I} (c : Chain (P i)) (n : ℕ) : (inj c) n = ⟨i, c n⟩

def OmegaCompletePartialOrder.Chain.Sigma.distrib {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] (c : Chain ((i : I) × P i)) : (i : I) × Chain (P i)

Converts a chain of coproducts into a coproduct of chains.

Equations

• OmegaCompletePartialOrder.Chain.Sigma.distrib c = ⟨(c 0).fst, { toFun := fun (n : ℕ) => have this := ⋯; ⋯ ▸ (c n).snd, monotone' := ⋯ }⟩

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sigma.distrib_inj {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] {i : I} (c : Chain (P i)) : distrib (inj c) = ⟨i, c⟩

@[simp]

theorem OmegaCompletePartialOrder.Chain.Sigma.inj_distrib {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] (c : Chain (Sigma P)) : inj (distrib c).snd = c

theorem OmegaCompletePartialOrder.Chain.Sigma.distrib_cases {I : Type u_1} {P : I → Type u_2} [(i : I) → Preorder (P i)] {p : Chain ((i : I) × P i) → Prop} (mk : ∀ {i : I} (c : Chain (P i)), p (inj c)) (c : Chain ((i : I) × P i)) : p c