le_partialEquivLimit — Mathlib

English

A directed limit of partial equivalences dominates each indexwise embedding.

Русский

Направленный предел частичных эквивалентностей доминирует каждое индексовое вложение.

LaTeX

$$$$ S i \\le partialEquivLimit S.$$$$

Lean4

theorem le_partialEquivLimit (i : ι) : S i ≤ partialEquivLimit S :=
  ⟨le_iSup (f := fun i ↦ (S i).dom) _,
    by
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
        these two `simp` calls cannot be combined. -/

    simp only [partialEquivLimit_comp_inclusion]
    simp only [cod_partialEquivLimit, ← Embedding.comp_assoc, subtype_comp_inclusion]⟩

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