notMem — Mathlib

English

If BoundaryLE holds at j, then for all k' with c'.Rel(e.f j) k', e.f a ≠ k' for every a.

Русский

Если BoundaryLE держится в j, то для всех k', удовлетворяющих c'.Rel(e.f j) k', выполняется e.f(a) ≠ k' для любого a.

LaTeX

$$BoundaryLE.notMem for Embedding$$

Lean4

theorem notMem {j : ι} (hj : e.BoundaryLE j) {k' : ι'} (hk' : c'.Rel (e.f j) k') (a : ι) : e.f a ≠ k' := fun ha =>
  hj.2 a (by simpa only [ha] using hk')

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