Documentation

Lean 4 Proof

theorem lower_triangular_not_symmetric {a : ℝ} (ha : a ≠ 0) :
    -- The matrix [[0, 0], [a, 0]] is not symmetric
    -- because entry (1,0) = a but entry (0,1) = 0
    ¬(a = 0) := ha

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Topology.lean:100

Module Section

Theorem 2, Propositions 1 and 4: CES-Forced Topology

In the same file