English
A gcongr-compatible variant asserting that if a1 ≤ a2, then algebraMap a1 ≤ algebraMap a2 in the target order.
Русский
Вариант gcongr: если a1 ≤ a2, то algebraMap a1 ≤ algebraMap a2 в целевом порядке.
LaTeX
$$$a_1 \le a_2 \Rightarrow \text{algebraMap } a_1 \le \text{algebraMap } a_2$$$
Lean4
/-- Extension for `algebraMap`. -/
@[positivity algebraMap _ _ _]
def evalAlgebraMap : PositivityExt where
eval {u β} _zβ _pβ
e := do
let ~q(@algebraMap $α _ $instα $instβ $instαβ $a) := e |
throwError"not `algebraMap`"
let pα ← synthInstanceQ q(PartialOrder $α)
match ← core q(inferInstance) pα a with
| .positive pa =>
let _instαSemiring ← synthInstanceQ q(Semiring $α)
let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
try
let _instβSemiring ← synthInstanceQ q(Semiring $β)
let _instβPartialOrder ← synthInstanceQ q(PartialOrder $β)
let _instβIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $β)
let _instαβsmul ← synthInstanceQ q(SMulPosStrictMono $α $β)
assertInstancesCommute
return .positive q(algebraMap_pos $β $pa)
catch _ =>
let _instβSemiring ← synthInstanceQ q(Semiring $β)
let _instβPartialOrder ← synthInstanceQ q(PartialOrder $β)
let _instβIsOrderedRing ← synthInstanceQ q(IsOrderedRing $β)
let _instαβsmul ← synthInstanceQ q(SMulPosMono $α $β)
assertInstancesCommute
return .nonnegative q(algebraMap_nonneg $β <| le_of_lt $pa)
| .nonnegative pa =>
let _instαSemiring ← synthInstanceQ q(CommSemiring $α)
let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
let _instβSemiring ← synthInstanceQ q(Semiring $β)
let _instβPartialOrder ← synthInstanceQ q(PartialOrder $β)
let _instβIsOrderedRing ← synthInstanceQ q(IsOrderedRing $β)
let _instαβsmul ← synthInstanceQ q(SMulPosMono $α $β)
assertInstancesCommute
return .nonnegative q(algebraMap_nonneg $β $pa)
| _ =>
pure .none
