LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Sigma #
Imported Lean Pool material for LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Sigma.
@[implicit_reducible]
instance
OmegaCompletePartialOrder.Sigma.instSigmaLeanPool
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → OmegaCompletePartialOrder (P i)]
:
OmegaCompletePartialOrder ((i : I) × P i)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
OmegaCompletePartialOrder.Sigma.ωSup_inj
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → OmegaCompletePartialOrder (P i)]
{i : I}
(c : Chain (P i))
: