mem_domain — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_domain {x : M} {c : ArchimedeanClass M} (hx : x ∈ seed.stratum c) : x ∈ f.val.domain :=
  by
  apply Set.mem_of_subset_of_mem f.prop.baseEmbedding_le.1
  apply seed.mem_domain_baseEmbedding hx

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