comapOn_dual_eq_of_bijOn — Mathlib

English

Dual of comapOn under bijection respects the dual operation: (N.comapOn E f)† = N†.comapOn E f.

Русский

Дуализация comapOn сохраняется под биекции: (N.comapOn E f)† = N†.comapOn E f.

LaTeX

$$$ (N.comapOn E f)^{\!*} = N^{\!*}.comapOn E f $$$

Lean4

theorem comapOn_dual_eq_of_bijOn (h : BijOn f E N.E) : (N.comapOn E f)✶ = N✶.comapOn E f :=
  by
  refine ext_isBase (by simp) (fun B hB ↦ ?_)
  rw [comapOn_isBase_iff_of_bijOn (by simpa), dual_isBase_iff, comapOn_isBase_iff_of_bijOn h, dual_isBase_iff _,
    comapOn_ground_eq, and_iff_left diff_subset, and_iff_left (by simpa), h.injOn.image_diff_subset (by simpa),
    h.image_eq]
  exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset

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