isExtensionPair_iff_cod — Mathlib

English

An isExtensionPair M N is equivalent to a condition that for every FG-equivalence f and m in M there exists an extension g with m in its codomain.

Русский

Пусть L.IsExtensionPair M N эквивалентно условию, что для каждого f и каждого m в M существует продолжение g с m в его кодом.

LaTeX

$$$L.IsExtensionPair\ M\ N \iff \forall f:\ L.FGEquiv N M\, \forall m\in M\, \exists g: (closure\ L\ {m}\cup S)\hookrightarrow N,\ f \le g.$$$

Lean4

theorem isExtensionPair_iff_cod : L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ g.1.cod ∧ f ≤ g := by
  refine Iff.intro ?_ ?_ <;>
    · intro h f m
      obtain ⟨g, h1, h2⟩ := h f.symm m
      exact ⟨g.symm, h1, monotone_symm h2⟩

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