ofSet — Mathlib

English

The source of the identity partial equivalence on a set s is s.

Русский

Источник тождественной частичной эквивалентности на множестве s равен s.

LaTeX

$$$\\text{ofSet}_\\text{source}(s) = s$$$

Lean4

/-- The identity partial equivalence on a set `s` -/
def ofSet (s : Set α) : PartialEquiv α α where
  toFun := id
  invFun := id
  source := s
  target := s
  map_source' _ hx := hx
  map_target' _ hx := hx
  left_inv' _ _ := rfl
  right_inv' _ _ := rfl

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