coe_pred_of_mem — Mathlib

English

If pred a.1 ∈ s, then (pred a).1 = pred a.1; i.e., pred commutes with embedding on members.

Русский

Если pred элемента принадлежит s, то значение pred через вложение соответствует pred на уровне α.

LaTeX

$$$$ \operatorname{pred}(a).1 = \operatorname{pred}(a.1) $$$$

Lean4

@[simp, norm_cast]
theorem coe_pred_of_mem [PredOrder α] {a : s} (h : pred a.1 ∈ s) : (pred a).1 = pred ↑a := by
  classical
  change Subtype.val (dite ..) = _
  simp [h]

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