setOf_dual_isBase_eq — Mathlib

English

The set of dual bases equals the image of the bases under complementation within E: {B | M✶.IsBase B} = (M.E \ ·) '' {B | M.IsBase B}.

Русский

Множество дуальных баз совпадает с образом базистной множества по дополнению внутри E: {B | M✶.IsBase B} = (M.E \ ·) '' {B | M.IsBase B}.

LaTeX

$${B | M✶.IsBase B} = (fun X \mapsto M.E \ X) '' {B | M.IsBase B}$$

Lean4

theorem setOf_dual_isBase_eq : {B | M✶.IsBase B} = (fun X ↦ M.E \ X) '' {B | M.IsBase B} :=
  by
  ext B
  simp only [mem_setOf_eq, mem_image, dual_isBase_iff']
  refine ⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩, fun ⟨B', hB', h⟩ ↦ ⟨?_, h.symm.trans_subset diff_subset⟩⟩
  rwa [← h, diff_diff_cancel_left hB'.subset_ground]

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