instIsStrictlySupportedTruncLE — Mathlib

English

If K is strictly supported with respect to e, then K.truncLE e is strictly supported with respect to any e'.

Русский

Если K строго поддержано относительно e, то K.truncLE e строго поддержано относительно любого e'.

LaTeX

$$$ (K.truncLE e).IsStrictlySupported e' $$$

Lean4

instance : (K.truncLE e).IsStrictlySupported e :=
  by
  rw [← isStrictlySupported_op_iff]
  exact inferInstanceAs ((K.op.truncGE e.op).IsStrictlySupported e.op)

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