English
A set t is the image of a set s under e if and only if for all x in the source, e(x) ∈ t iff x ∈ s.
Русский
Множество t является образом множества s под e тогда и только тогда, когда для всех x из источника e(x) ∈ t эквивалентно x ∈ s.
LaTeX
$$$\\mathrm{IsImage}(e, s, t) \\;\\equiv\\; \\forall x \\in \\mathrm{source}(e), (e(x) \\in t \\leftrightarrow x \\in s)$$$
Lean4
/-- We say that `t : Set Y` is an image of `s : Set X` under an open partial homeomorphism `e`
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 X) (t : Set Y) : Prop :=
∀ ⦃x⦄, x ∈ e.source → (e x ∈ t ↔ x ∈ s)
