lift' — Mathlib

English

If f has a HasBasis p s and h is monotone, then f.lift' h has a HasBasis p (h ∘ s).

Русский

Если у f есть база HasBasis p s и h монотонна, то у f.lift' h есть база p (h ∘ s).

LaTeX

$$$ \\text{hf} : f.HasBasis p\\ s \\;\\; \\text{hh} : \\text{Monotone } h \\quad \\Rightarrow\\quad (f.lift' h).HasBasis p (h \\circ s) $$$

Lean4

theorem lift' {ι} {p : ι → Prop} {s} (hf : f.HasBasis p s) (hh : Monotone h) : (f.lift' h).HasBasis p (h ∘ s) :=
  ⟨fun t =>
    (hf.mem_lift_iff (fun i => hasBasis_principal (h (s i))) (monotone_principal.comp hh)).trans <| by
      simp only [exists_const, true_and, comp]⟩

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