Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Isomorphism of two marked relations

Lax604544.RelationIsomorphism · concepts/Lax604544/RelationIsomorphism.lean · lax-604544

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Given two subsets PVP_V and HVH_V of a set and two binary relations PEP_E and HEH_E on it, the marked relations are isomorphic when some map restricts to a bijection from PVP_V onto HVH_V such that, for x,y∈PVx, y \in P_V, PE(x,y)P_E(x, y) holds if and only if HE(f(x),f(y))H_E(f(x), f(y)) does.

    Concept map
    1 concept; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Logic.Basic
    2
    3/-!
    4---
    5title: Isomorphism of two marked relations
    6type: definition
    7---
    8Given two subsets PVP_V and HVH_V of a set and two binary relations PEP_E
    9and HEH_E on it, the marked relations are isomorphic when some map restricts
    10to a bijection from PVP_V onto HVH_V such that, for x,y∈PVx, y \in P_V,
    11PE(x,y)P_E(x, y) holds if and only if HE(f(x),f(y))H_E(f(x), f(y)) does.
    12-/
    13
    14namespace Lax604544.RelationIsomorphism
    15
    16section Generic
    17
    18variable {A : Type}
    19
    20/-- Some map is a bijection of the `PV`-vertices onto the `HV`-vertices
    21carrying `PE`-edges to `HE`-edges *and back*: an isomorphism of the two marked
    22graphs. -/
    23def RelIsoOn (PV HV : A → Prop) (PE HE : A → A → Prop) : Prop :=
    24 ∃ f : A → A, (∀ x, PV x → HV (f x)) ∧
    25 (∀ x y, PV x → PV y → f x = f y → x = y) ∧
    26 (∀ y, HV y → ∃ x, PV x ∧ f x = y) ∧
    27 ∀ x y, PV x → PV y → (PE x y ↔ HE (f x) (f y))
    28
    29end Generic
    30
    31end Lax604544.RelationIsomorphism
    32
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…