injective_iff — Mathlib

English

A function f: Bool → α is injective if and only if f(false) ≠ f(true).

Русский

Функция f: Bool → α инъективна тогда и только тогда, когда f(ложь) ≠ f(истина).

LaTeX

$$$ \forall {\alpha : \text{Sort}*} {f : Bool \to \alpha},\; \mathrm{Injective}(f) \leftrightarrow f(\text{false}) \neq f(\text{true}) $$$

Lean4

@[simp]
theorem injective_iff {α : Sort*} {f : Bool → α} : Function.Injective f ↔ f false ≠ f true :=
  ⟨fun Hinj Heq ↦ false_ne_true (Hinj Heq), fun H x y ↦ by grind [cases Bool]⟩

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