1. Physlib
  2. Units
  3. WithDim
  4. Area
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Units.WithDim.Basic

Area

In this module we define the dimensionful type corresponding to an area. We define specific instances of areas, such as square meters, square feet, etc.

@[expose] public section

The type of areas in the absence of a choice of unit.

abbrev DimArea : Type := Dimensionful (WithDim (L𝓭 * L𝓭) ℝ≥0)

Basic areas

Area in SI units

@[simp] lemma squareMeter_in_SI : squareMeter.1 SI = ⟨1⟩ := ⊢ ↑squareMeter SI = { val := 1 } All goals completed! 🐙@[simp] lemma squareFoot_in_SI : squareFoot.1 SI = ⟨0.09290304⟩ := ⊢ ↑squareFoot SI = { val := 9290304e-8 } ⊢ ⟨0.3048, ⋯⟩ ^ (1 + 1) • { val := 1 } = { val := 9290304e-8 } ⊢ ↑(⟨0.3048, ⋯⟩ ^ (1 + 1) • { val := 1 }).val = ↑{ val := 9290304e-8 }.val ⊢ ↑⟨0.3048, ⋯⟩ ^ (1 + 1) = 9290304e-8 All goals completed! 🐙@[simp] lemma squareMile_in_SI : squareMile.1 SI = ⟨2589988.110336⟩ := ⊢ ↑squareMile SI = { val := 2589988.110336 } ⊢ ⟨1609.344, ⋯⟩ ^ (1 + 1) • { val := 1 } = { val := 2589988.110336 } ⊢ ↑(⟨1609.344, ⋯⟩ ^ (1 + 1) • { val := 1 }).val = ↑{ val := 2589988.110336 }.val ⊢ ↑⟨1609.344, ⋯⟩ ^ (1 + 1) = 2589988.110336 All goals completed! 🐙@[simp] lemma are_in_SI : are.1 SI = ⟨100⟩ := ⊢ ↑are SI = { val := 100 } All goals completed! 🐙@[simp] lemma hectare_in_SI : hectare.1 SI = ⟨10000⟩ := ⊢ ↑hectare SI = { val := 10000 } All goals completed! 🐙@[simp] lemma acre_in_SI : acre.1 SI = ⟨4046.8564224⟩ := ⊢ ↑acre SI = { val := 4046.8564224 } ⊢ ⟨1609.344, ⋯⟩ ^ (1 + 1) • { val := 640⁻¹ } = { val := 4046.8564224 } ⊢ ↑(⟨1609.344, ⋯⟩ ^ (1 + 1) • { val := 640⁻¹ }).val = ↑{ val := 4046.8564224 }.val ⊢ ↑⟨1609.344, ⋯⟩ ^ (1 + 1) * 640⁻¹ = 4046.8564224 All goals completed! 🐙

## Relations between areas

One acre is exactly 43560 square feet.

lemma acre_eq_mul_squareFeet : acre = (43560 : ℝ≥0) • squareFoot := ⊢ acre = 43560 • squareFoot ⊢ (toDimensionful SI).symm acre = (toDimensionful SI).symm (43560 • squareFoot) ⊢ ↑((toDimensionful SI).symm acre).val = ↑((toDimensionful SI).symm (43560 • squareFoot)).val All goals completed! 🐙