mapEquiv_eq_map — Mathlib

English

IsBase and IsBasis are preserved under equivalence mapping: (M.mapEquiv f).IsBase B iff M.IsBase (f.symm '' B).

Русский

Базисность сохраняется при отображении по эквивалентности: (M.mapEquiv f).IsBase B эквивалентно M.IsBase (f.symm '' B).

LaTeX

$$$(M.mapEquiv f).IsBase B \iff M.IsBase (f.symm '' B)$$$

Lean4

theorem mapEquiv_eq_map (f : α ≃ β) : M.mapEquiv f = M.map f f.injective.injOn :=
  rfl

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