mem_domain_baseEmbedding — Mathlib

English

If x lies in seed.stratum c, then x belongs to the domain of seed.baseEmbedding.

Русский

Если x лежит в слое c семени, то x принадлежит области определения базового вложения семени.

LaTeX

$$$ x \in seed.stratum c \Rightarrow x \in seed.baseEmbedding.domain $$$

Lean4

theorem mem_domain_baseEmbedding {x : M} {c : ArchimedeanClass M} (h : x ∈ seed.stratum c) :
    x ∈ seed.baseEmbedding.domain := by
  apply Set.mem_of_mem_of_subset h
  rw [domain_baseEmbedding]
  simpa using le_iSup_iff.mpr fun _ h ↦ h c

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