comap_isBase_iff — Mathlib

English

The IsBase for comap is equivalent to the image-based IsBasis with injOn and subset conditions.

Русский

Эквивалентность IsBase для comap и образованной IsBasis с условиями injOn и подмножества.

LaTeX

$$∀ {B : Set α}, (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ B.InjOn f ∧ B ⊆ f ⁻¹' N.E$$

Lean4

@[simp]
theorem comap_isBase_iff {B : Set α} :
    (N.comap f).IsBase B ↔ N.IsBasis (f '' B) (f '' (f ⁻¹' N.E)) ∧ B.InjOn f ∧ B ⊆ f ⁻¹' N.E := by
  rw [← isBasis_ground_iff, comap_isBasis_iff]; rfl

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