mono — Mathlib

English

If f is a decomposition on A with witness S, and A' ⊆ A, and f and f' agree on A', then f' is a decomposition on A' with the same witness S.

Русский

Если f—декомпозиция на A со свидетелем S, и A' ⊆ A, и f и f' совпадают на A', то f' является декомпозициией на A' с тем же свидетелем S.

LaTeX

$$$\mono : IsDecompOn(f,A,S) \to A' \subseteq A \to EqOn(f,f',A') \to IsDecompOn(f',A',S).$$$

Lean4

theorem mono {f f' : X → X} {A A' : Set X} {S : Finset G} (h : IsDecompOn f A S) (hA' : A' ⊆ A) (hf' : EqOn f f' A') :
    IsDecompOn f' A' S := by
  intro a ha
  rw [← hf' ha]
  exact h a (hA' ha)

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