isoProd — Mathlib

English

The equivalence defined above is an order isomorphism between IntegrationParams and the product type.

Русский

Указанная эквивалентность образует тождество порядка между IntegrationParams и произведением типов.

LaTeX

$$$\\text{equivProd} \\text{ preserves order, i.e. } l_1 \\le l_2 \\iff (\\text{equivProd } l_1) \\le (\\text{equivProd } l_2).$$$

Lean4

/-- Auxiliary `OrderIso` with a product type used to lift a `BoundedOrder` structure. -/
def isoProd : IntegrationParams ≃o Bool × Boolᵒᵈ × Boolᵒᵈ :=
  ⟨equivProd, Iff.rfl⟩

Похожие утверждения