IsImage — Mathlib

English

IsImage s t holds for e if and only if for every x in e.source, e x ∈ t ⇔ x ∈ s.

Русский

IsImage s t выполняется для e тогда и только тогда, когда для всякого x ∈ source(e) выполняется e x ∈ t ⇔ x ∈ s.

LaTeX

$$IsImage(e, s, t) := ∀ x ∈ e.source, e x ∈ t ⇔ x ∈ s$$

Lean4

/-- We say that `t : Set β` is an image of `s : Set α` under a partial equivalence if
any of the following equivalent conditions hold:

* `e '' (e.source ∩ s) = e.target ∩ t`;
* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
-/
def IsImage (s : Set α) (t : Set β) : Prop :=
  ∀ ⦃x⦄, x ∈ e.source → (e x ∈ t ↔ x ∈ s)

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