restrictSubtype_dual' — Mathlib

English

If E is the ground set of M (i.e., E = M.E), then the dual of the restriction to E equals the restriction to E of the dual: (M|E)^* = M^*|E.

Русский

Если E является базовым множеством M (то есть E = M.E), то двойственный ограничение к E равно ограничению двойственного к M к E: (M|E)^* = M^*|E.

LaTeX

$$$ (M|_E)^* = M^*|_E \\; \\text{(when } E = M.E \\text{)} $$$

Lean4

theorem restrictSubtype_dual' (hM : M.E = E) : (M.restrictSubtype E)✶ = M✶.restrictSubtype E := by
  rw [← hM, restrictSubtype_dual]

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