Lax Lean Archive

Triangles

Lax68.Triangles · concepts/Lax68/Triangles.lean · lax-68

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

    Triangle graph illustration
    Triangle graph illustration

    A triangle is a finite complete graph on exactly three vertices.

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

    In the paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Maps
    2
    3/-!
    4---
    5title: Triangles
    6type: definition
    7---
    8
    9![Triangle graph illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/4dd917c8b9a1e181ec951b7f6fa384262af31fa9/planar-graph-classes-v4-33/assets/triangle.svg "Triangle graph illustration")
    10
    11A triangle is a finite complete graph on exactly three vertices.
    12-/
    13
    14set_option autoImplicit false
    15
    16namespace Lax68.Triangles
    17
    18def IsTriangle {V : Type*} (G : SimpleGraph V) : Prop :=
    19 Nonempty (G ≃g SimpleGraph.completeGraph (Fin 3))
    20
    21end Lax68.Triangles
    22
    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…