mem_iff — Mathlib

English

If f maps s to t and s^c maps to t^c, then for all x, f x ∈ t iff x ∈ s.

Русский

Если f отображает s в t и s^c в t^c, тогда ∀x, f x ∈ t ⇔ x ∈ s.

LaTeX

$$$\\\\MapsTo f s t \\\\land \\\\MapsTo f (s^{\\\\mathsf{c}}) (t^{\\\\mathsf{c}}) \\\\rightarrow \\\\forall x, f x \\in t \\\\leftrightarrow x \\in s$$$

Lean4

theorem mem_iff (h : MapsTo f s t) (hc : MapsTo f sᶜ tᶜ) {x} : f x ∈ t ↔ x ∈ s :=
  ⟨fun ht => by_contra fun hs => hc hs ht, fun hx => h hx⟩

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